rank_quotient_add_rank_of_divisionRing

English

For any subspace p of V over K, dim(V) = dim(V/p) + dim(p).

Русский

Для любого подпространства p пространства V верно: dim(V) = dim(V/p) + dim(p).

LaTeX

$$$\operatorname{Module.rank}_K(V) = \operatorname{Module.rank}_K(V/p) + \operatorname{Module.rank}_K(p)$$$

Lean4

/-- Also see `rank_quotient_add_rank`. -/
theorem rank_quotient_add_rank_of_divisionRing (p : Submodule K V) :
    Module.rank K (V ⧸ p) + Module.rank K p = Module.rank K V := by
  classical
  let ⟨f⟩ := quotient_prod_linearEquiv p
  exact rank_prod'.symm.trans f.rank_eq

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