card_eq_finrank_add_one — Mathlib

English

If ι is finite and b is an affine basis, then |ι| equals finrank(k,V) plus one.

Русский

Если ι конечно, и b — аффинная база, то |ι| = finrank_k(V) + 1.

LaTeX

$$Fintype.card ι = Module.finrank k V + 1$$

Lean4

theorem card_eq_finrank_add_one [Fintype ι] (b : AffineBasis ι k P) : Fintype.card ι = Module.finrank k V + 1 :=
  have : FiniteDimensional k V := b.finiteDimensional
  b.ind.affineSpan_eq_top_iff_card_eq_finrank_add_one.mp b.tot

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