Submodule.card_quotient_mul_card_quotient

theorem Submodule.card_quotient_mul_card_quotient : ∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (S T : Submodule R M), T ≤ S → ∀ [inst_3 : DecidablePred fun x => x ∈ Submodule.map T.mkQ S] [inst_4 : Fintype (M ⧸ S)] [inst_5 : Fintype (M ⧸ T)], Fintype.card ↥(Submodule.map T.mkQ S) * Fintype.card (M ⧸ S) = Fintype.card (M ⧸ T)

This theorem, named `Submodule.card_quotient_mul_card_quotient`, is a corollary of the third isomorphism theorem in the context of modules over a ring. It states that for any ring `R`, additive commutative group `M`, and `R`-module structure on `M`, given two submodules `S` and `T` of `M` where `T` is a subset of `S`, the product of the number of elements of the submodule of `S` mapped by `T` and the number of elements in the quotient of `M` by `S` is equal to the number of elements in the quotient of `M` by `T`. This is expressed in mathematical notation as `[S : T] * [M : S] = [M : T]`. The condition that `T` is a subset of `S` is required. The statement of the theorem also assumes decidability of the membership of the mapped elements in the submodule of `S` and the finiteness of the quotient sets `M/S` and `M/T`.

More concisely: For any ring `R`, additive commutative group `M` with an `R`-module structure, and submodules `S` and `T` of `M` with `T` a subset of `S`, the product of the index of `T` in `S` and the index of `M` in `S` equals the index of `M` in `T`. That is, `[S : T] * [M : S] = [M : T]`.