Module docstring
{"# Lemmas about semiconjugate elements of a group
"}
SemiconjBy.inv_inv_symm_iff
theorem
: SemiconjBy a⁻¹ x⁻¹ y⁻¹ ↔ SemiconjBy a y x
Full source
@[to_additive (attr := simp)]
theorem inv_inv_symm_iff : SemiconjBySemiconjBy a⁻¹ x⁻¹ y⁻¹ ↔ SemiconjBy a y x := by
simp_rw [SemiconjBy, ← mul_inv_rev, inv_inj, eq_comm]Informal description
For elements $a, x, y$ in a division monoid, the relation $\text{SemiconjBy}(a^{-1}, x^{-1}, y^{-1})$ holds if and only if $\text{SemiconjBy}(a, y, x)$ holds. Here, $\text{SemiconjBy}(a, x, y)$ means that $a \cdot x = y \cdot a$.
SemiconjBy.inv_symm_left_iff
theorem
: SemiconjBy a⁻¹ y x ↔ SemiconjBy a x y
Full source
@[to_additive (attr := simp)] lemma inv_symm_left_iff : SemiconjBySemiconjBy a⁻¹ y x ↔ SemiconjBy a x y := by
simp_rw [SemiconjBy, eq_mul_inv_iff_mul_eq, mul_assoc, inv_mul_eq_iff_eq_mul, eq_comm]Informal description
For elements $a, x, y$ in a group $G$, the relation $a^{-1} \cdot y = x \cdot a^{-1}$ holds if and only if $a \cdot x = y \cdot a$ holds.
SemiconjBy.inv_right_iff
theorem
: SemiconjBy a x⁻¹ y⁻¹ ↔ SemiconjBy a x y
Full source
@[to_additive (attr := simp)] lemma inv_right_iff : SemiconjBySemiconjBy a x⁻¹ y⁻¹ ↔ SemiconjBy a x y := by
rw [← inv_symm_left_iff, inv_inv_symm_iff]Informal description
For elements $a, x, y$ in a group $G$, the relation $a \cdot x^{-1} = y^{-1} \cdot a$ holds if and only if $a \cdot x = y \cdot a$ holds.
SemiconjBy.zpow_right
theorem
(h : SemiconjBy a x y) : ∀ m : ℤ, SemiconjBy a (x ^ m) (y ^ m)
Full source
@[to_additive (attr := simp)] lemma zpow_right (h : SemiconjBy a x y) :
∀ m : ℤ, SemiconjBy a (x ^ m) (y ^ m)
| (n : ℕ) => by simp [zpow_natCast, h.pow_right n]
| .negSucc n => by
simp only [zpow_negSucc, inv_right_iff]
apply pow_right hInformal description
For elements $a, x, y$ in a group $G$, if $a$ semiconjugates $x$ to $y$ (i.e., $a x = y a$), then for any integer $m$, $a$ semiconjugates $x^m$ to $y^m$ (i.e., $a x^m = y^m a$).