Theorems · Theorem · linear algebra

Submodule.finrank_sup_add_finrank_inf_eq

∀ {K : Type u} {V : Type v} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
  (s t : Submodule K V) [FiniteDimensional K ↥s] [FiniteDimensional K ↥t],
  Module.finrank K ↥(s ⊔ t) + Module.finrank K ↥(s ⊓ t) = Module.finrank K ↥s + Module.finrank K ↥t

The sum of the dimensions of s + t and s ∩ t is the sum of the dimensions of s and t

Defined in

Mathlib.LinearAlgebra.FiniteDimensional.Lemmas

Cited by

12 results in Mathlib

Foundations

Depth 117 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

DivisionRingAddCommGroupModuleFiniteDimensionalFiniteDimensional