Theorems · Theorem · number theory

MulChar.apply_mem_rootsOfUnity_of_pow_eq_one

∀ {F : Type u_1} [inst : Field F] [Finite F] {R : Type u_2} [inst_2 : CommRing R] {χ : MulChar F R} {n : ℕ},
  χ ^ n = 1 → ∀ {a : F}, a ≠ 0 → ∃ ζ ∈ rootsOfUnity n R, ↑ζ = χ a

The non-zero values of a multiplicative character χ such that χ^n = 1 are nth roots of unity.

Defined in

Mathlib.NumberTheory.MulChar.Lemmas

Cited by

2 results in Mathlib

Foundations

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

Assumes

FieldFiniteCommRing