DirichletCharacter.factorsThrough_conductor
theorem DirichletCharacter.factorsThrough_conductor :
∀ {R : Type u_1} [inst : CommMonoidWithZero R] {n : ℕ} (χ : DirichletCharacter R n), χ.FactorsThrough χ.conductor
This theorem states that for any commutative monoid with zero `R`, any natural number `n`, and any Dirichlet character `χ` of level `n` over `R`, the Dirichlet character `χ` factors through its conductor. In other words, the conductor of `χ`, which is the smallest natural number `m` such that `χ` is periodic on integers modulo `m`, divides `n` and there exists a Dirichlet character `χ₀` of level `m` such that `χ` is equivalent to `χ₀` applied to the mapping from integers modulo `n` to integers modulo `m`.
More concisely: Given a commutative monoid with zero `R`, any Dirichlet character `χ` of level `n` over `R` factors through its conductor `m`, i.e., `χ` is equivalent to some Dirichlet character `χ₀` of level `m` on integers modulo `n`.
|
DirichletCharacter.FactorsThrough.dvd
theorem DirichletCharacter.FactorsThrough.dvd :
∀ {R : Type u_1} [inst : CommMonoidWithZero R] {n : ℕ} {χ : DirichletCharacter R n} {d : ℕ},
χ.FactorsThrough d → d ∣ n
This theorem states that for any type `R` that is a commutative monoid with zero, any natural number `n`, any Dirichlet character `χ` of level `n` over `R`, and any natural number `d`, if `χ` factors through a Dirichlet character at level `d`, then `d` divides `n`. In other words, if a Dirichlet character at a certain level can be expressed in terms of a Dirichlet character at a lower level, then the lower level divides the higher one.
More concisely: If a Dirichlet character of level `n` over a commutative monoid with zero factors through a Dirichlet character of level `d`, then `d` divides `n`.
|
DirichletCharacter.FactorsThrough.eq_changeLevel
theorem DirichletCharacter.FactorsThrough.eq_changeLevel :
∀ {R : Type u_1} [inst : CommMonoidWithZero R] {n : ℕ} {χ : DirichletCharacter R n} {d : ℕ}
(h : χ.FactorsThrough d), χ = (DirichletCharacter.changeLevel ⋯) h.χ₀
The theorem `DirichletCharacter.FactorsThrough.eq_changeLevel` states that for any type `R` with a commutative zero-preserving multiplication operation, any natural number `n`, and any Dirichlet character `χ` of level `n`, if `χ` factors through a Dirichlet character of level `d`, then `χ` is equivalent to this character after modifying its level to `d` using the `DirichletCharacter.changeLevel` function. This theorem reveals the relationship between Dirichlet characters and their factorization levels in the context of number theory.
More concisely: If a Dirichlet character of level `n` factors through a character of level `d`, then it is equal to the character obtained by changing the level of the former to `d`.
|
DirichletCharacter.level_one
theorem DirichletCharacter.level_one :
∀ {R : Type u_1} [inst : CommMonoidWithZero R] (χ : DirichletCharacter R 1), χ = 1
This theorem states that for any type `R` that has an instance of the `CommMonoidWithZero` structure, any Dirichlet character of level `1` over `R` is actually equivalent to `1`. In other words, if you have a Dirichlet character defined over a commutative monoid with zero, and the level of this character is `1`, then this character is essentially the constant function that always returns `1`.
More concisely: For any commutative monoid with zero `R`, every Dirichlet character of level 1 over `R` is the trivial character, i.e., maps all elements to 1.
|