card_eq_card_units_of_hasEnoughRootsOfUnity

English

The cardinality of MulChar M R equals the cardinality of Mˣ under suitable hypotheses.

Русский

Число элементов MulChar M R равно числу единиц Mˣ при подходящих условиях.

LaTeX

$$card (MulChar M R) = card (Mˣ)$$

Lean4

/-- The cardinality of the group of `R`-valued multiplicative characters on a finite commutative
monoid `M` is the same as that of its unit group `Mˣ` when `R` is a ring that has enough roots
of unity. -/
theorem card_eq_card_units_of_hasEnoughRootsOfUnity : Nat.card (MulChar M R) = Nat.card Mˣ :=
  Nat.card_congr (mulEquiv_units M R).some.toEquiv

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