finrank_sup_add_finrank_inf_eq — Mathlib

English

If V is finite-dimensional and h is a basis with index set ι, then (finrank_K V) cast to Cardinal equals the cardinality of ι.

Русский

Если V конечномерно и базис h имеет индексное множество ι, то (finrank_K V) в кардиналах равно кардинальности ι.

LaTeX

$$(\mathrm{finrank}_K V : \mathrm{Cardinal}) = #ι$$

Lean4

/-- The sum of the dimensions of s + t and s ∩ t is the sum of the dimensions of s and t -/
theorem finrank_sup_add_finrank_inf_eq (s t : Submodule K V) [FiniteDimensional K s] [FiniteDimensional K t] :
    finrank K ↑(s ⊔ t) + finrank K ↑(s ⊓ t) = finrank K ↑s + finrank K ↑t :=
  by
  have key : Module.rank K ↑(s ⊔ t) + Module.rank K ↑(s ⊓ t) = Module.rank K s + Module.rank K t :=
    rank_sup_add_rank_inf_eq s t
  repeat rw [← finrank_eq_rank] at key
  norm_cast at key

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