Theorems · Theorem · number theory

DirichletCharacter.primitiveCharacter_changeLevel_apply

∀ {R : Type u_1} [inst : CommMonoidWithZero R] {n : ℕ} [Nontrivial R] {m : ℕ} [NeZero m] (hm : n ∣ m)
  (χ : DirichletCharacter R n) (a : ℤ),
  ((DirichletCharacter.changeLevel hm) χ).primitiveCharacter ↑a = χ.primitiveCharacter ↑a

The primitive character of changeLevel hm χ is equal to the primitive character of χ. This is stated as a pointwise equality because the equality of Dirichlet characters does not typecheck.

Defined in

Mathlib.NumberTheory.DirichletCharacter.Basic

Cited by

1 results in Mathlib

Foundations

Depth 92 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommMonoidWithZeroNontrivialNeZero