Theorems · Theorem · linear algebra

HasRankNullity.rank_quotient_add_rank

∀ {R : Type v} {inst : Ring R} [self : HasRankNullity.{u, v} R] {M : Type u} [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] (N : Submodule R M), Module.rank R (M ⧸ N) + Module.rank R ↥N = Module.rank R M

Defined in

Mathlib.LinearAlgebra.Dimension.RankNullity

Cited by

2 results in Mathlib

Foundations

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

Assumes

HasRankNullityAddCommGroupModule