isUnit_mul_iff — Mathlib

English

Same as isUnit_mul_iff: for commuting a,b, IsUnit (a b) is equivalent to IsUnit a and IsUnit b.

Русский

То же самое, что и isUnit_mul_iff: при коммутировании a,b IsUnit(a b) эквивалентно IsUnit a и IsUnit b.

LaTeX

$$IsUnit (a b) \Leftrightarrow (IsUnit a \land IsUnit b) \text{ при } Commute(a,b)$$

Lean4

@[to_additive]
theorem isUnit_mul_iff (h : Commute a b) : IsUnit (a * b) ↔ IsUnit a ∧ IsUnit b :=
  ⟨fun ⟨u, hu⟩ => ⟨(u.leftOfMul a b hu.symm h).isUnit, (u.rightOfMul a b hu.symm h).isUnit⟩, fun H => H.1.mul H.2⟩

Похожие утверждения