finrank_add_eq_of_isCompl — Mathlib

English

Let K be a division ring, V a finite-dimensional K-vector space, and U, W be subspaces of V that form a direct sum decomposition V = U ⊕ W. Then the dimension (rank) of U plus the dimension of W equals the dimension of V.

Русский

Пусть K — делимость кольцо, V конечномерное векторное пространство над K, и U, W — подпространства V, удовлетворяющие V = U ⊕ W. Тогда dim_K U + dim_K W = dim_K V.

LaTeX

$$$\\operatorname{finrank}_K(U) + \\operatorname{finrank}_K(W) = \\operatorname{finrank}_K(V) \\quad\\text{if } U \\oplus W = V.$$$

Lean4

theorem finrank_add_eq_of_isCompl [FiniteDimensional K V] {U W : Submodule K V} (h : IsCompl U W) :
    finrank K U + finrank K W = finrank K V :=
  by
  rw [← finrank_sup_add_finrank_inf_eq, h.codisjoint.eq_top, h.disjoint.eq_bot, finrank_bot, add_zero]
  exact finrank_top _ _

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