isUnit_iff — Mathlib

English

If a and b are associates, then a is a unit if and only if b is a unit.

Русский

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

LaTeX

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

Lean4

theorem isUnit_iff [Monoid M] {a b : M} (h : a ~ᵤ b) : IsUnit a ↔ IsUnit b :=
  ⟨h.isUnit, h.symm.isUnit⟩

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