Theorems · Definition · number theory

DirichletCharacter.FactorsThrough

{R : Type u_1} → [inst : CommMonoidWithZero R] → {n : ℕ} → DirichletCharacter R n → ℕ → Prop

χ of level n factors through a Dirichlet character χ₀ of level d if d ∣ n and χ₀ = χ ∘ (ZMod n → ZMod d).

Defined in

Mathlib.NumberTheory.DirichletCharacter.Basic

Cited by

13 results in Mathlib

Foundations

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

Assumes

CommMonoidWithZero