isUnit — Mathlib

English

If a and b are associates in a monoid and a is a unit, then b is a unit.

Русский

Если a и b ассоциированы в моноиде и a является единицей, то b тоже единица.

LaTeX

$$$$\mathrm{Associated}(a,b) \Rightarrow (\mathrm{IsUnit}(a) \Rightarrow \mathrm{IsUnit}(b)).$$$$

Lean4

protected theorem isUnit [Monoid M] {a b : M} (h : a ~ᵤ b) : IsUnit a → IsUnit b :=
  let ⟨u, hu⟩ := h
  fun ⟨v, hv⟩ => ⟨v * u, by simp [hv, hu.symm]⟩

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