Theorems · Definition · number theory

MulChar.ofRootOfUnity

{M : Type u_1} →
  [inst : CommMonoid M] →
    [inst_1 : Fintype M] →
      [inst_2 : DecidableEq M] →
        {R : Type u_2} →
          [inst_3 : CommMonoidWithZero R] →
            {ζ : Rˣ} →
              ζ ∈ rootsOfUnity (Fintype.card Mˣ) R → {g : Mˣ} → (∀ (x : Mˣ), x ∈ Subgroup.zpowers g) → MulChar M R

Given a finite monoid M with unit group Mˣ cyclic of order n and an nth root of unity ζ in R, there is a multiplicative character M → R that sends a given generator of Mˣ to ζ.

Defined in

Mathlib.NumberTheory.MulChar.Lemmas

Cited by

2 results in Mathlib

Foundations

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

Assumes

CommMonoidFintypeDecidableEqCommMonoidWithZero