isUnit_iff_exists_and_exists — Mathlib

English

An element a is a unit iff there exist b and c with a·b = 1 and c·a = 1.

Русский

Элемент a является единицей тогда и только тогда, когда существуют b и c такие, что a·b = 1 и c·a = 1.

LaTeX

$$IsUnit(a) \iff (\exists b, a \cdot b = 1) \land (\exists c, c \cdot a = 1)$$

Lean4

/-- See `isUnit_iff_exists` for a similar lemma with one existential. -/
@[to_additive /-- See `isAddUnit_iff_exists` for a similar lemma with one existential. -/
    ]
theorem isUnit_iff_exists_and_exists [Monoid M] {a : M} : IsUnit a ↔ (∃ b, a * b = 1) ∧ (∃ c, c * a = 1) :=
  isUnit_iff_exists.trans
    ⟨fun ⟨b, hba, hab⟩ => ⟨⟨b, hba⟩, ⟨b, hab⟩⟩, fun ⟨⟨b, hb⟩, ⟨_, hc⟩⟩ => ⟨b, hb, left_inv_eq_right_inv hc hb ▸ hc⟩⟩

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