Dedekind's group matrix has rank at least $|G| - 1$ when all nontrivial character sums are nonzero

This is the rank form of Dedekind's group determinant for a finite abelian group.

Let $G$ be a finite abelian group of order $n$, and let $F$ be a field that contains a primitive $n$-th root of unity (so that the group of $n$-th roots of unity of $F$ is cyclic of order $n$ and the characters $\chi : G \to F^\times$ number exactly $n$). For a function $f : G \to F$ form the group matrix

For a character $\chi$ of $G$ with values in $F^\times$, the vector $(\chi(\tau))_{\tau \in G}$ is an eigenvector of $A_f$ with eigenvalue the character sum $\sum_{\rho \in G} \chi(\rho)^{-1} f(\rho)$; Dedekind's formula $\det A_f = \prod_\chi \sum_\rho \chi(\rho) f(\rho)$ is the determinant form of this decomposition. The statement here is the consequence for the rank:

If the character sum $\displaystyle\sum_{\sigma \in G} \chi(\sigma)\, f(\sigma)$ is nonzero for every nontrivial character $\chi$ of $G$, then

The trivial character is excluded on purpose: its character sum $\sum_\sigma f(\sigma)$ may vanish, and it does vanish in the intended application (logarithms of the Galois conjugates of a unit, whose sum is the logarithm of a norm). The bound $n - 1$ is therefore the right one.

Use. In the proof of Leopoldt's conjecture for abelian fields, $G$ is the Galois group, $f(\sigma) = \log_p(\sigma\varepsilon)$ for a Minkowski unit $\varepsilon$, and the nonvanishing of the nontrivial character sums is Brumer's theorem; the rank bound then gives $n - 1 = \operatorname{rank}\mathcal{O}_K^\times$ independent rows. See Leopoldt.charSum_log_ne_zero_of_brumer and Leopoldt.exists_linearIndependent_log_conj_of_card_sub_one_le_rank.

Formalization Note. $G$ is a Group with IsMulCommutative, matching the Galois group K ≃ₐ[ℚ] K of an abelian extension; a proof may build a local CommGroup instance. The roots-of-unity hypothesis is Mathlib's HasEnoughRootsOfUnity F (Fintype.card G); it implies that the characteristic of $F$ does not divide $n$, and with HasEnoughRootsOfUnity.of_dvd and Monoid.exponent_dvd_card it gives CommGroup.card_monoidHom_of_hasEnoughRootsOfUnity, the count of characters. Characters are G →* Fˣ and are linearly independent by linearIndependent_monoidHom. The matrix is Matrix.of fun σ τ => f (σ * τ⁻¹) and the rank is Matrix.rank over $F$; the subtraction $n - 1$ is truncated natural-number subtraction, which is harmless since $n \ge 1$.