English
Given a unit u and elements a,b with a b = u and a,b commute, there exists a unit whose value is b and whose inverse is a u^{-1}. This expresses a natural decomposition of the unit u into a right factor.
Русский
Пусть есть единица u и элементы a, b такие, что a b = u и a, b коммутируют. Тогда существует единица w с w.val = b и w.inv = a u^{-1}.
LaTeX
$$∃ w ∈ Mˣ, w.val = b ∧ w.inv = a · u^{-1} \text{ при } a b = u
\land Commute(a,b)$$
Lean4
/-- If the product of two commuting elements is a unit, then the right multiplier is a unit. -/
@[to_additive /-- If the sum of two commuting elements is an additive unit, then the right summand
is an additive unit. -/
]
def rightOfMul (u : Mˣ) (a b : M) (hu : a * b = u) (hc : Commute a b) : Mˣ :=
u.leftOfMul b a (hc.eq ▸ hu) hc.symm
