Ranges of multiplicative characters #
To show that a multiplicative character takes values in a subset containing zero, it suffices to check the values on units. This applies, for example, to subfields and subrings containing the character values on units, since a multiplicative character vanishes on nonunits.
theorem
MulChar.apply_mem_of_forall_unit
{R : Type u_1}
{R' : Type u_2}
{S : Type u_3}
[CommMonoid R]
[CommMonoidWithZero R']
[SetLike S R']
[ZeroMemClass S R']
(χ : MulChar R R')
(s : S)
(hχ : ∀ (u : Rˣ), χ ↑u ∈ s)
(a : R)
:
A multiplicative character takes values in a subset containing 0 whenever all its values
on units lie there.