Theorems · Theorem · number theory

DirichletCharacter.conductor_changeLevel

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

The conductor is invariant under changeLevel: lifting a Dirichlet character χ of level n to a multiple level m does not change its conductor.

Defined in

Mathlib.NumberTheory.DirichletCharacter.Basic

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommMonoidWithZeroNeZero