fintype — Mathlib

English

If a free module is finite, then the index set of any basis is finite.

Русский

Если свободный модуль конечен, то множество индексов любого базиса конечно.

LaTeX

$$$$ \exists \iota\,\big( \mathrm{Finite}(\iota) \land \exists b: \mathrm{Basis}(\iota, R, M) \big) $$$$

Lean4

/-- If a free module is finite, then the arbitrary basis is finite. -/
noncomputable instance fintype (R : Type u) (M : Type v) [Semiring R] [AddCommMonoid M] [Module R M] [Module.Free R M]
    [Module.Finite R M] : Fintype (Module.Free.ChooseBasisIndex R M) :=
  by
  refine @Fintype.ofFinite _ ?_
  cases subsingleton_or_nontrivial R
  · have := Module.subsingleton R M
    rw [ChooseBasisIndex]
    infer_instance
  · exact Module.Finite.finite_basis (chooseBasis _ _)

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