3.2. Vanishing in degree 0🔗

Proposition3.2.1

uses 1used by 1✓L∃∀N

B_{0,\chi} = 0 for non-trivial \chi. Let R be an integral domain and let \chi be a Dirichlet character modulo N \ge 1 valued in R with \chi \ne \mathbf{1}. Then B_{0,\chi} = 0.

Definition 3.1.1

Lean code for Proposition3.2.1●1 theorem

theoremdefined in BernoulliRegular/BernoulliGeneralized.lean

complete

theorem BernoulliRegular.BernoulliGen_zero_of_ne_one.{u_1} {N : ℕ}
  {R : Type u_1} [CommRing R] [Algebra ℚ R] [IsDomain R] [NeZero N]
  {χ : DirichletCharacter R N} (hχ : χ ≠ 1) :
  BernoulliRegular.BernoulliGen χ 0 = 0

theorem BernoulliRegular.BernoulliGen_zero_of_ne_one.{u_1}
  {N : ℕ} {R : Type u_1} [CommRing R]
  [Algebra ℚ R] [IsDomain R] [NeZero N]
  {χ : DirichletCharacter R N}
  (hχ : χ ≠ 1) :
  BernoulliRegular.BernoulliGen χ 0 = 0

For a non-trivial Dirichlet character `χ` over a domain `R`,
`B_{0, χ} = 0`. Follows from `Polynomial.bernoulli 0 = 1` and the
character-sum identity (our T004).

Proof for Proposition 3.2.1

uses 0

The polynomial B_0(X) = 1 is the constant polynomial, so its evaluation at a/N equals 1 and the algebra map sends it to 1 \in R. Substituting into the definition, B_{0,\chi} = \sum_{a \in \mathbb{Z}/N\mathbb{Z}} \chi(a). For any non-trivial character \chi of a finite abelian group, this character sum vanishes: pick b with \chi(b) \ne 1 and observe that the substitution a \mapsto a b multiplies the sum by \chi(b), which is only consistent with \chi(b) \cdot \Sigma = \Sigma if \Sigma = 0, since 1 - \chi(b) is a nonzero element of the integral domain R.