Theorems · Definition · number theory

IsCyclotomicExtension.zeta

(n : ℕ) →
  [NeZero n] →
    (A : Type w) →
      (B : Type z) →
        [inst : CommRing A] → [inst_1 : CommRing B] → [inst_2 : Algebra A B] → [IsCyclotomicExtension {n} A B] → B

If B is an n-th cyclotomic extension of A, then zeta n A B is a primitive root of unity in B.

Defined in

Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots

Cited by

27 results in Mathlib

Foundations

Depth 19 from the axioms · uses propext, Classical.choice

Assumes

NeZeroCommRingCommRingAlgebraIsCyclotomicExtension