unique — Mathlib

English

If a basis of a ring R over itself is indexed by ι, then ι is a unique type (has exactly one element).

Русский

Если базис кольца R над самим R индексирован типом ι, то ι является уникальным типом (один элемент).

LaTeX

$$Unique ι$$

Lean4

/-- Given a basis of a ring over itself indexed by a type `ι`, then `ι` is `Unique`. -/
noncomputable def _root_.Module.Basis.unique {ι : Type*} (b : Basis ι R R) : Unique ι :=
  by
  have : Cardinal.mk ι = ↑(Module.finrank R R) := (Module.mk_finrank_eq_card_basis b).symm
  have : Subsingleton ι ∧ Nonempty ι := by simpa [Cardinal.eq_one_iff_unique]
  exact Nonempty.some ((unique_iff_subsingleton_and_nonempty _).2 this)

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