isUnit_iff_exists — Mathlib

English

For any unit u, its underlying element is a unit: IsUnit(u.val).

Русский

Для любого единичного элемента u его основанный элемент является единицей: IsUnit(u.val).

LaTeX

$$$IsUnit(u^{\text{val}})$$$

Lean4

/-- See `isUnit_iff_exists_and_exists` for a similar lemma with two existentials. -/
@[to_additive /-- See `isAddUnit_iff_exists_and_exists` for a similar lemma with two existentials. -/
    ]
theorem isUnit_iff_exists [Monoid M] {x : M} : IsUnit x ↔ ∃ b, x * b = 1 ∧ b * x = 1 :=
  by
  refine ⟨fun ⟨u, hu⟩ => ?_, fun ⟨b, h1b, h2b⟩ => ⟨⟨x, b, h1b, h2b⟩, rfl⟩⟩
  subst x
  exact ⟨u.inv, u.val_inv, u.inv_val⟩

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