Rank is additive along a tower of submodules

For submodules p ≤ q ≤ r of a module M, the relative quotient r / p is filtered by q / p, and TauCeti.rank_quotient_submoduleOf_tower records that its rank is the sum of the ranks of the two steps. Relative quotients are spelled with Submodule.submoduleOf, so that q / p means ↥q ⧸ p.submoduleOf q.

The proof is Noether's third isomorphism theorem (Submodule.quotientQuotientEquivQuotient) together with rank–nullity, which is why the base ring is asked only for HasRankNullity.

theorem TauCeti.rank_quotient_submoduleOf_tower {R : Type v} {M : Type u} [Ring R] [AddCommGroup M] [Module R M] [HasRankNullity.{u, v} R] {p q r : Submodule R M} (hpq : p ≤ q) (hqr : q ≤ r) : Module.rank R (↥r ⧸ p.submoduleOf r) = Module.rank R (↥q ⧸ p.submoduleOf q) + Module.rank R (↥r ⧸ q.submoduleOf r)

Rank is additive along a tower p ≤ q ≤ r of submodules: the relative quotients of the two steps add up to the relative quotient of the composite. This is Noether's third isomorphism theorem together with rank–nullity.