basisUnique — Mathlib

English

A free module of rank 1 has a basis indexed by a type with a unique element.

Русский

Свободный модуль ранга 1 имеет базис, индексированный типом с единственным элементом.

LaTeX

$$$$ \\exists ι:\\text{Basis } ι\\;R\\;M \\text{, где } ι \\text{ уникален} $$$$

Lean4

/-- A free module with rank 1 has a basis with one element. -/
noncomputable def basisUnique (ι : Type*) [Unique ι] (h : finrank R M = 1) : Basis ι R M :=
  haveI : Module.Finite R M := Module.finite_of_finrank_pos (_root_.zero_lt_one.trans_le h.symm.le)
  (finBasisOfFinrankEq R M h).reindex (Equiv.ofUnique _ _)

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