card_eq_card_quotient_mul_card — Mathlib

English

For a submodule S of a module M with finite cardinality, the cardinality of M equals the product of the cardinality of S and the cardinality of the quotient M/S:

Русский

Для подмодуля S модуля M с конечной мощностью выполняется |M| = |S| · |M/S|.

LaTeX

$$$|M| = |S| \cdot |M/S|,$$$

Lean4

theorem card_eq_card_quotient_mul_card (S : Submodule R M) : Nat.card M = Nat.card S * Nat.card (M ⧸ S) :=
  by
  rw [mul_comm, ← Nat.card_prod]
  exact Nat.card_congr AddSubgroup.addGroupEquivQuotientProdAddSubgroup

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