English
If α is finite, then the number of circle-valued characters equals the number of elements of α:
Русский
Если α конечна, то число окружностных символов равно числу элементов α.
LaTeX
$$$ \#(AddChar(\alpha, \mathbb{C})) = \#(\alpha) $$$
Lean4
@[simp]
theorem card_eq [Fintype α] : card (AddChar α ℂ) = card α :=
by
obtain ⟨ι, _, n, hn, ⟨e⟩⟩ := AddCommGroup.equiv_directSum_zmod_of_finite' α
classical
have hn' i : NeZero (n i) := by have := hn i; exact ⟨by positivity⟩
let f : α → AddChar α ℂ := fun a ↦ coeHom.compAddChar ((mkZModAux n <| e a).compAddMonoidHom e)
have hf : Injective f :=
circleEquivComplex.injective.comp
((compAddMonoidHom_injective_left _ e.surjective).comp <|
mkZModAux_injective.comp <| DFunLike.coe_injective.comp <| e.injective.comp Additive.ofMul.injective)
exact (card_addChar_le _ _).antisymm (Fintype.card_le_of_injective _ hf)
