rank_quotient_add_rank_of_isDomain

theorem rank_quotient_add_rank_of_isDomain : ∀ {R : Type u} {M : Type v} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] [inst_3 : IsDomain R] (M' : Submodule R M), Module.rank R (M ⧸ M') + Module.rank R ↥M' = Module.rank R M

This is a statement of the **rank-nullity theorem** for commutative domains in Lean 4. Specifically, it states that for any commutative ring `R`, any additive commutative group `M` that is also a module over `R`, and any submodule `M'` of `M` (with `R` being a domain), the rank of the quotient module `M ⧸ M'` plus the rank of the submodule `M'` is equal to the rank of the original module `M`.

More concisely: For any commutative ring `R`, any additive commutative group `M` that is an `R`-module, and any submodule `M'` of `M` with `R` being a domain, the rank of the quotient module `M/M'` is equal to the sum of the ranks of `M` and `M'`.