Theorems · Theorem · linear algebra

rank_add_rank_split

∀ {K : Type u} {V V₁ V₂ V₃ : Type v} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
  [inst_3 : AddCommGroup V₁] [inst_4 : Module K V₁] [inst_5 : AddCommGroup V₂] [inst_6 : Module K V₂]
  [inst_7 : AddCommGroup V₃] [inst_8 : Module K V₃] (db : V₂ →ₗ[K] V) (eb : V₃ →ₗ[K] V) (cd : V₁ →ₗ[K] V₂)
  (ce : V₁ →ₗ[K] V₃),
  ⊤ ≤ db.range ⊔ eb.range →
    cd.ker = ⊥ →
      db ∘ₗ cd = eb ∘ₗ ce →
        (∀ (d : V₂) (e : V₃), db d = eb e → ∃ c, cd c = d ∧ ce c = e) →
          Module.rank K V + Module.rank K V₁ = Module.rank K V₂ + Module.rank K V₃

This is mostly an auxiliary lemma for Submodule.rank_sup_add_rank_inf_eq.

Defined in

Mathlib.LinearAlgebra.Dimension.DivisionRing

Cited by

0 results in Mathlib

Foundations

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

Assumes

DivisionRingAddCommGroupModuleAddCommGroupModuleAddCommGroupModuleAddCommGroupModule