card_quotient_mul_card_quotient — Mathlib

English

Corollary: card(S.map T.mkQ) · card(M/S) = card(M/T).

Русский

Следствие: кардинал. числа соответствуют: |S.map T.mkQ| · |M/S| = |M/T|.

LaTeX

$$$$\\lvert S.map(T.mkQ)\\rvert \\cdot \\lvert M/S \\rvert = \\lvert M/T \\rvert$$$$

Lean4

/-- Corollary of the third isomorphism theorem: `[S : T] [M : S] = [M : T]` -/
theorem card_quotient_mul_card_quotient (S T : Submodule R M) (hST : T ≤ S) :
    Nat.card (S.map T.mkQ) * Nat.card (M ⧸ S) = Nat.card (M ⧸ T) := by
  rw [Submodule.card_eq_card_quotient_mul_card (map T.mkQ S),
    Nat.card_congr (quotientQuotientEquivQuotient T S hST).toEquiv]

Похожие утверждения