card_range — Mathlib

English

The range of sumCongrHom has the same cardinality as the product of permutation groups on α and β.

Русский

Образ sumCongrHom имеет такую же мощность, как произведение групп перестановок на α и β.

LaTeX

$$$\\mathrm{Fintype.card}(\\mathrm{range}(\\mathrm{sumCongrHom}(\\alpha,\\beta))) = \\mathrm{Fintype.card}(\\mathrm{Perm}(\\alpha) \\times \\mathrm{Perm}(\\beta))$$$

Lean4

@[simp]
theorem card_range {α β : Type*} [Fintype (sumCongrHom α β).range] [Fintype (Perm α × Perm β)] :
    Fintype.card (sumCongrHom α β).range = Fintype.card (Perm α × Perm β) :=
  Fintype.card_eq.mpr ⟨(ofInjective (sumCongrHom α β) sumCongrHom_injective).symm⟩

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