card_eq_card_quotient_mul_card_subgroup

English

There is a canonical equivalence between α ⧸ ⊥ and α.

Русский

Существует каноническое эквивалентное отображение между α ⧸ ⊥ и α.

LaTeX

$$$\\text{QuotientEquivSelf}(α) : α/⊥ ≃ α$$$

Lean4

@[to_additive AddSubgroup.card_eq_card_quotient_mul_card_addSubgroup]
theorem card_eq_card_quotient_mul_card_subgroup (s : Subgroup α) : Nat.card α = Nat.card (α ⧸ s) * Nat.card s := by
  rw [← Nat.card_prod]; exact Nat.card_congr Subgroup.groupEquivQuotientProdSubgroup

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