isUnit_iff — Mathlib

English

In Finset, an equality IsUnit s ⇔ ∃ a, s = {a} ∧ IsUnit a holds: a finite set is a unit exactly when it is a singleton of a unit element.

Русский

В Finset множество является единицей тогда и только тогда, когда оно — синглетон из единицы элемента.

LaTeX

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

Lean4

@[to_additive (attr := simp)]
theorem isUnit_iff : IsUnit s ↔ ∃ a, s = { a } ∧ IsUnit a :=
  by
  constructor
  · rintro ⟨u, rfl⟩
    obtain ⟨a, b, ha, hb, h⟩ := Finset.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.finset

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