English
If a and b commute, then a b is a unit precisely when a and b are units.
Русский
Если a и b коммутируют, то a b является единицей тогда и только тогда, когда a и b являются единицами.
LaTeX
$$IsUnit (a b) \Leftrightarrow (IsUnit a \land IsUnit b) \text{ при } Commute(a,b)$$
Lean4
/-- If the product of two commuting elements is a unit, then the left multiplier is a unit. -/
@[to_additive /-- If the sum of two commuting elements is an additive unit, then the left summand is
an additive unit. -/
]
def leftOfMul (u : Mˣ) (a b : M) (hu : a * b = u) (hc : Commute a b) : Mˣ
where
val := a
inv := b * ↑u⁻¹
val_inv := by rw [← mul_assoc, hu, u.mul_inv]
inv_val := by
have : Commute a u := hu ▸ (Commute.refl _).mul_right hc
rw [← this.units_inv_right.right_comm, ← hc.eq, hu, u.mul_inv]
