Mathlib.Algebra.GroupWithZero.Semiconj

SemiconjBy.zero_right theorem

[MulZeroClass G₀] (a : G₀) : SemiconjBy a 0 0

Full source

@[simp]
theorem zero_right [MulZeroClass G₀] (a : G₀) : SemiconjBy a 0 0 := by
  simp only [SemiconjBy, mul_zero, zero_mul]

Zero is self-semiconjugate under any element in a group with zero

Informal description

For any element $a$ in a multiplicative structure with zero $G₀$, the zero element is semiconjugate to itself by $a$, i.e., $a * 0 = 0 * a$.

SemiconjBy.zero_left theorem

[MulZeroClass G₀] (x y : G₀) : SemiconjBy 0 x y

Full source

@[simp]
theorem zero_left [MulZeroClass G₀] (x y : G₀) : SemiconjBy 0 x y := by
  simp only [SemiconjBy, mul_zero, zero_mul]

Zero Semiconjugates Any Two Elements in a MulZeroClass

Informal description

In a multiplicative structure with zero $G₀$ (i.e., a `MulZeroClass`), for any elements $x$ and $y$ in $G₀$, the zero element $0$ semiconjugates $x$ to $y$, meaning that $0 * x = y * 0$ holds.

SemiconjBy.inv_symm_left_iff₀ theorem

: SemiconjBy a⁻¹ x y ↔ SemiconjBy a y x

Full source

@[simp]
theorem inv_symm_left_iff₀ : SemiconjBySemiconjBy a⁻¹ x y ↔ SemiconjBy a y x :=
  Classical.by_cases (fun ha : a = 0 => by simp only [ha, inv_zero, SemiconjBy.zero_left]) fun ha =>
    @units_inv_symm_left_iff _ _ (Units.mk0 a ha) _ _

Equivalence of Semiconjugacy Relations via Inversion: $a^{-1} \cdot x = y \cdot a^{-1} \leftrightarrow a \cdot y = x \cdot a$

Informal description

For any elements $a, x, y$ in a group with zero, the following are equivalent: 1. $a^{-1}$ semiconjugates $x$ to $y$ (i.e., $a^{-1} * x = y * a^{-1}$) 2. $a$ semiconjugates $y$ to $x$ (i.e., $a * y = x * a$)

SemiconjBy.inv_symm_left₀ theorem

(h : SemiconjBy a x y) : SemiconjBy a⁻¹ y x

Full source

theorem inv_symm_left₀ (h : SemiconjBy a x y) : SemiconjBy a⁻¹ y x :=
  SemiconjBy.inv_symm_left_iff₀.2 h

Inversion of Semiconjugacy Relation in a Group with Zero

Informal description

Let $M$ be a group with zero. If an element $a \in M$ semiconjugates $x$ to $y$ (i.e., $a \cdot x = y \cdot a$), then the inverse $a^{-1}$ semiconjugates $y$ to $x$ (i.e., $a^{-1} \cdot y = x \cdot a^{-1}$).

SemiconjBy.inv_right₀ theorem

(h : SemiconjBy a x y) : SemiconjBy a x⁻¹ y⁻¹

Full source

theorem inv_right₀ (h : SemiconjBy a x y) : SemiconjBy a x⁻¹ y⁻¹ := by
  by_cases ha : a = 0
  · simp only [ha, zero_left]
  by_cases hx : x = 0
  · subst x
    simp only [SemiconjBy, mul_zero, @eq_comm _ _ (y * a), mul_eq_zero] at h
    simp [h.resolve_right ha]
  · have := mul_ne_zero ha hx
    rw [h.eq, mul_ne_zero_iff] at this
    exact @units_inv_right _ _ _ (Units.mk0 x hx) (Units.mk0 y this.1) h

Inversion Preserves Semiconjugacy in a Group with Zero

Informal description

Let $M$ be a group with zero. If $a \in M$ semiconjugates $x$ to $y$ (i.e., $a * x = y * a$), then $a$ also semiconjugates $x^{-1}$ to $y^{-1}$ (i.e., $a * x^{-1} = y^{-1} * a$).

SemiconjBy.inv_right_iff₀ theorem

: SemiconjBy a x⁻¹ y⁻¹ ↔ SemiconjBy a x y

Full source

@[simp]
theorem inv_right_iff₀ : SemiconjBySemiconjBy a x⁻¹ y⁻¹ ↔ SemiconjBy a x y :=
  ⟨fun h => inv_inv x ▸ inv_inv y ▸ h.inv_right₀, inv_right₀⟩

Semiconjugacy of Inverses in a Group with Zero: $a * x^{-1} = y^{-1} * a \leftrightarrow a * x = y * a$

Informal description

For elements $a, x, y$ in a group with zero, the element $a$ semiconjugates $x^{-1}$ to $y^{-1}$ if and only if $a$ semiconjugates $x$ to $y$. In other words, $a * x^{-1} = y^{-1} * a$ holds if and only if $a * x = y * a$ holds.

SemiconjBy.div_right theorem

(h : SemiconjBy a x y) (h' : SemiconjBy a x' y') : SemiconjBy a (x / x') (y / y')

Full source

theorem div_right (h : SemiconjBy a x y) (h' : SemiconjBy a x' y') :
    SemiconjBy a (x / x') (y / y') := by
  rw [div_eq_mul_inv, div_eq_mul_inv]
  exact h.mul_right h'.inv_right₀

Division of Semiconjugate Pairs in a Group with Zero

Informal description

Let $G$ be a group with zero. If an element $a \in G$ semiconjugates $x$ to $y$ (i.e., $a x = y a$) and $x'$ to $y'$ (i.e., $a x' = y' a$), then $a$ semiconjugates $x / x'$ to $y / y'$ (i.e., $a (x / x') = (y / y') a$), where division is defined as $x / x' = x \cdot x'^{-1}$.

SemiconjBy.zpow_right₀ theorem

{a x y : G₀} (h : SemiconjBy a x y) : ∀ m : ℤ, SemiconjBy a (x ^ m) (y ^ m)

Full source

lemma zpow_right₀ {a x y : G₀} (h : SemiconjBy a x y) : ∀ m : ℤ, SemiconjBy a (x ^ m) (y ^ m)
  | (n : ℕ) => by simp [h.pow_right n]
  | .negSucc n => by simp only [zpow_negSucc, (h.pow_right (n + 1)).inv_right₀]

Integer Powers Preserve Semiconjugacy in a Group with Zero: $a \cdot x^m = y^m \cdot a$

Informal description

Let $G₀$ be a group with zero, and let $a, x, y \in G₀$ such that $x$ is semiconjugate to $y$ by $a$ (i.e., $a \cdot x = y \cdot a$). Then for any integer $m$, the $m$-th power of $x$ is semiconjugate to the $m$-th power of $y$ by $a$, i.e., $a \cdot x^m = y^m \cdot a$.

Commute.zpow_right₀ theorem

(h : Commute a b) : ∀ m : ℤ, Commute a (b ^ m)

Full source

lemma zpow_right₀ (h : Commute a b) : ∀ m : ℤ, Commute a (b ^ m) := SemiconjBy.zpow_right₀ h

Commutation with Integer Powers in a Group with Zero: $a \cdot b^m = b^m \cdot a$

Informal description

Let $G₀$ be a group with zero, and let $a, b \in G₀$ such that $a$ and $b$ commute (i.e., $a \cdot b = b \cdot a$). Then for any integer $m$, the element $a$ commutes with the $m$-th power of $b$, i.e., $a \cdot b^m = b^m \cdot a$.

Commute.zpow_left₀ theorem

(h : Commute a b) (m : ℤ) : Commute (a ^ m) b

Full source

lemma zpow_left₀ (h : Commute a b) (m : ℤ) : Commute (a ^ m) b := (h.symm.zpow_right₀ m).symm

Commutation of Integer Powers in a Group with Zero: $a^m \cdot b = b \cdot a^m$

Informal description

Let $G₀$ be a group with zero, and let $a, b \in G₀$ such that $a$ and $b$ commute (i.e., $a \cdot b = b \cdot a$). Then for any integer $m$, the $m$-th power of $a$ commutes with $b$, i.e., $a^m \cdot b = b \cdot a^m$.

Commute.zpow_zpow₀ theorem

(h : Commute a b) (m n : ℤ) : Commute (a ^ m) (b ^ n)

Full source

lemma zpow_zpow₀ (h : Commute a b) (m n : ℤ) : Commute (a ^ m) (b ^ n) :=
  (h.zpow_left₀ m).zpow_right₀ n

Commutation of Integer Powers in a Group with Zero: $a^m \cdot b^n = b^n \cdot a^m$

Informal description

Let $G₀$ be a group with zero, and let $a, b \in G₀$ such that $a$ and $b$ commute (i.e., $a \cdot b = b \cdot a$). Then for any integers $m$ and $n$, the $m$-th power of $a$ commutes with the $n$-th power of $b$, i.e., $a^m \cdot b^n = b^n \cdot a^m$.

Commute.zpow_self₀ theorem

(a : G₀) (n : ℤ) : Commute (a ^ n) a

Full source

lemma zpow_self₀ (a : G₀) (n : ℤ) : Commute (a ^ n) a := (Commute.refl a).zpow_left₀ n

Commutation of Element with Its Own Integer Power in a Group with Zero: $a^n \cdot a = a \cdot a^n$

Informal description

For any element $a$ in a group with zero $G₀$ and any integer $n$, the $n$-th power of $a$ commutes with $a$, i.e., $a^n \cdot a = a \cdot a^n$.

Commute.self_zpow₀ theorem

(a : G₀) (n : ℤ) : Commute a (a ^ n)

Full source

lemma self_zpow₀ (a : G₀) (n : ℤ) : Commute a (a ^ n) := (Commute.refl a).zpow_right₀ n

Self-Commutation with Integer Powers in a Group with Zero

Informal description

For any element $a$ in a group with zero $G₀$ and any integer $n$, the element $a$ commutes with its own $n$-th power, i.e., $a \cdot a^n = a^n \cdot a$.

Commute.zpow_zpow_self₀ theorem

(a : G₀) (m n : ℤ) : Commute (a ^ m) (a ^ n)

Full source

lemma zpow_zpow_self₀ (a : G₀) (m n : ℤ) : Commute (a ^ m) (a ^ n) :=
  (Commute.refl a).zpow_zpow₀ m n

Commutation of Integer Powers of the Same Element in a Group with Zero: $a^m \cdot a^n = a^n \cdot a^m$

Informal description

For any element $a$ in a group with zero $G₀$ and any integers $m$ and $n$, the $m$-th power of $a$ commutes with the $n$-th power of $a$, i.e., $a^m \cdot a^n = a^n \cdot a^m$.