Lemmas about semiconjugate elements of a group #
@[simp]
theorem
AddSemiconjBy.neg_neg_symm_iff
{G : Type u_1}
[SubtractionMonoid G]
{a : G}
{x : G}
{y : G}
:
AddSemiconjBy (-a) (-x) (-y) ↔ AddSemiconjBy a y x
@[simp]
theorem
SemiconjBy.inv_inv_symm_iff
{G : Type u_1}
[DivisionMonoid G]
{a : G}
{x : G}
{y : G}
:
SemiconjBy a⁻¹ x⁻¹ y⁻¹ ↔ SemiconjBy a y x
theorem
SemiconjBy.inv_inv_symm
{G : Type u_1}
[DivisionMonoid G]
{a : G}
{x : G}
{y : G}
:
SemiconjBy a y x → SemiconjBy a⁻¹ x⁻¹ y⁻¹
Alias of the reverse direction of SemiconjBy.inv_inv_symm_iff.
theorem
AddSemiconjBy.neg_neg_symm
{G : Type u_1}
[SubtractionMonoid G]
{a : G}
{x : G}
{y : G}
:
AddSemiconjBy a y x → AddSemiconjBy (-a) (-x) (-y)
@[simp]
theorem
AddSemiconjBy.neg_symm_left_iff
{G : Type u_1}
[AddGroup G]
{a : G}
{x : G}
{y : G}
:
AddSemiconjBy (-a) y x ↔ AddSemiconjBy a x y
@[simp]
theorem
SemiconjBy.inv_symm_left_iff
{G : Type u_1}
[Group G]
{a : G}
{x : G}
{y : G}
:
SemiconjBy a⁻¹ y x ↔ SemiconjBy a x y
theorem
SemiconjBy.inv_symm_left
{G : Type u_1}
[Group G]
{a : G}
{x : G}
{y : G}
:
SemiconjBy a x y → SemiconjBy a⁻¹ y x
Alias of the reverse direction of SemiconjBy.inv_symm_left_iff.
theorem
AddSemiconjBy.neg_symm_left
{G : Type u_1}
[AddGroup G]
{a : G}
{x : G}
{y : G}
:
AddSemiconjBy a x y → AddSemiconjBy (-a) y x
@[simp]
theorem
AddSemiconjBy.neg_right_iff
{G : Type u_1}
[AddGroup G]
{a : G}
{x : G}
{y : G}
:
AddSemiconjBy a (-x) (-y) ↔ AddSemiconjBy a x y
@[simp]
theorem
SemiconjBy.inv_right_iff
{G : Type u_1}
[Group G]
{a : G}
{x : G}
{y : G}
:
SemiconjBy a x⁻¹ y⁻¹ ↔ SemiconjBy a x y
theorem
SemiconjBy.inv_right
{G : Type u_1}
[Group G]
{a : G}
{x : G}
{y : G}
:
SemiconjBy a x y → SemiconjBy a x⁻¹ y⁻¹
Alias of the reverse direction of SemiconjBy.inv_right_iff.
theorem
AddSemiconjBy.neg_right
{G : Type u_1}
[AddGroup G]
{a : G}
{x : G}
{y : G}
:
AddSemiconjBy a x y → AddSemiconjBy a (-x) (-y)
@[simp]
theorem
AddSemiconjBy.zsmul_right
{G : Type u_1}
[AddGroup G]
{a : G}
{x : G}
{y : G}
(h : AddSemiconjBy a x y)
(m : ℤ)
:
AddSemiconjBy a (m • x) (m • y)
abbrev
AddSemiconjBy.zsmul_right.match_1
(motive : ℤ → Prop)
:
∀ (x : ℤ), (∀ (n : ℕ), motive (Int.ofNat n)) → (∀ (n : ℕ), motive (Int.negSucc n)) → motive x
Equations
- ⋯ = ⋯
Instances For
@[simp]
theorem
SemiconjBy.zpow_right
{G : Type u_1}
[Group G]
{a : G}
{x : G}
{y : G}
(h : SemiconjBy a x y)
(m : ℤ)
:
SemiconjBy a (x ^ m) (y ^ m)
theorem
AddSemiconjBy.eq_zero_iff
{G : Type u_1}
[AddGroup G]
(a : G)
{x : G}
{y : G}
(h : AddSemiconjBy a x y)
:
theorem
SemiconjBy.eq_one_iff
{G : Type u_1}
[Group G]
(a : G)
{x : G}
{y : G}
(h : SemiconjBy a x y)
: