Theorems · Theorem · number theory

DirichletCharacter.factorsThrough_gcd

∀ {R : Type u_1} [inst : CommMonoidWithZero R] {n : ℕ} (χ : DirichletCharacter R n) {m : ℕ} [NeZero n]
  (ψ : DirichletCharacter R m),
  (DirichletCharacter.changeLevel ⋯) χ = (DirichletCharacter.changeLevel ⋯) ψ → χ.FactorsThrough (n.gcd m)

Let χ and ψ be Dirichlet characters of level n and m respectively. Assume that they agree at level n * m. Then χ factors through gcd(n, m).

Defined in

Mathlib.NumberTheory.DirichletCharacter.Basic

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommMonoidWithZeroNeZero