isUnit_iff — Mathlib

English

Equivalently, IsUnit s holds if and only if s is a singleton {a} and a is a unit.

Русский

Эквивалентно: IsUnit s тогда и только тогда, когда s — одиночное {a} и a — единица.

LaTeX

$$IsUnit s ↔ ∃ a, s = { a } ∧ IsUnit a$$

Lean4

@[to_additive (attr := simp 500)]
theorem isUnit_iff : IsUnit s ↔ ∃ a, s = { a } ∧ IsUnit a :=
  by
  constructor
  · rintro ⟨u, rfl⟩
    obtain ⟨a, b, ha, hb, h⟩ := Set.mul_eq_one_iff.1 u.mul_inv
    refine ⟨a, ha, ⟨a, b, h, singleton_injective ?_⟩, rfl⟩
    rw [← singleton_mul_singleton, ← ha, ← hb]
    exact u.inv_mul
  · rintro ⟨a, rfl, ha⟩
    exact ha.set

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