Commute.units_inv_right
theorem Commute.units_inv_right : ∀ {M : Type u_1} [inst : Monoid M] {a : M} {u : Mˣ}, Commute a ↑u → Commute a ↑u⁻¹
This theorem states that for any type `M` equipped with a monoid structure, and any elements `a` of `M` and `u` which is a unit in `M`, if `a` and `u` commute (meaning that multiplying `a` and `u` is the same as multiplying `u` and `a`), then `a` also commutes with the inverse of `u`. In other words, if `a * u = u * a`, then it's also true that `a * u^-1 = u^-1 * a`.
More concisely: If `a` is an element of a monoid `M` with unit `u`, and `a` commutes with `u` (i.e., `a * u = u * a`), then `a` commutes with the inverse of `u` (i.e., `a * u^-1 = u^-1 * a`).
|
isUnit_pow_iff
theorem isUnit_pow_iff : ∀ {M : Type u_1} [inst : Monoid M] {n : ℕ} {a : M}, n ≠ 0 → (IsUnit (a ^ n) ↔ IsUnit a) := by
sorry
The theorem `isUnit_pow_iff` states that for any type `M` that forms a Monoid and any non-zero natural number `n`, an element `a` of the Monoid `M` is a unit if and only if `a` raised to the power `n` is a unit. A unit in this context is defined as an element that has a two-sided inverse.
More concisely: For any monoid M and natural number n greater than 0, an element a of M is a unit if and only if a^n is a unit.
|