Theorems · Theorem · number theory

MulChar.eq_iff

∀ {R : Type u_1} [inst : CommMonoid R] {R' : Type u_3} [inst_1 : CommMonoidWithZero R'] {g : Rˣ},
  (∀ (x : Rˣ), x ∈ Subgroup.zpowers g) → ∀ (χ₁ χ₂ : MulChar R R'), χ₁ = χ₂ ↔ χ₁ ↑g = χ₂ ↑g

Two multiplicative characters on a monoid whose unit group is generated by g are equal if and only if they agree on g.

Defined in

Mathlib.NumberTheory.MulChar.Lemmas

Cited by

0 results in Mathlib

Foundations

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

Assumes

CommMonoidCommMonoidWithZero