ofRankEqZero — Mathlib

English

If rank K V = 0, then there exists a Basis ι K V for some empty ι.

Русский

Если rank K V = 0, то существует Basis ι K V для некоторого пустого типа ι.

LaTeX

$$$$ \\exists ι:\\text{IsEmpty } ι \\rightarrow \\text{Basis } ι\\;K\\;V $$$$

Lean4

/-- The `ι` indexed basis on `V`, where `ι` is an empty type and `V` is zero-dimensional.

See also `Module.finBasis`.
-/
noncomputable def ofRankEqZero [Module.Free K V] {ι : Type*} [IsEmpty ι] (hV : Module.rank K V = 0) : Basis ι K V :=
  haveI : Subsingleton V := by
    obtain ⟨_, b⟩ := Module.Free.exists_basis (R := K) (M := V)
    haveI := mk_eq_zero_iff.1 (hV ▸ b.mk_eq_rank'')
    exact b.repr.toEquiv.subsingleton
  Basis.empty _

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