English
The sum of the trivial character over a finite ring equals the number of units: ∑ a 1(a) = |Rˣ|.
Русский
Сумма тривиального символа по кольцу равна числу единиц: ∑ a 1(a) = |Rˣ|.
LaTeX
$$∑ a, (1 : MulChar R R') a = card Rˣ$$
Lean4
/-- The sum over all values of the trivial multiplicative character on a finite ring is
the cardinality of its unit group. -/
theorem sum_one_eq_card_units [DecidableEq R] : (∑ a, (1 : MulChar R R') a) = Fintype.card Rˣ :=
by
calc
(∑ a, (1 : MulChar R R') a) = ∑ a : R, if IsUnit a then 1 else 0 := Finset.sum_congr rfl fun a _ => ?_
_ = ((Finset.univ : Finset R).filter IsUnit).card := (Finset.sum_boole _ _)
_ = (Finset.univ.map ⟨((↑) : Rˣ → R), Units.val_injective⟩).card := ?_
_ = Fintype.card Rˣ := congr_arg _ (Finset.card_map _)
· split_ifs with h
· exact one_apply_coe h.unit
· exact map_nonunit _ h
· congr
ext a
simp [IsUnit]
