Theorems · Theorem · linear algebra

rank_quotient_add_rank_of_isDomain

∀ {R : Type uR} {M : Type uM} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] [IsDomain R]
  (M' : Submodule R M), Module.rank R (M ⧸ M') + Module.rank R ↥M' = Module.rank R M

The rank-nullity theorem for commutative domains. Also see rank_quotient_add_rank.

Defined in

Mathlib.LinearAlgebra.Dimension.Localization

Cited by

0 results in Mathlib

Foundations

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

Assumes

CommRingAddCommGroupModuleIsDomain