Theorems · Theorem · number theory

IsCyclotomicExtension.aeval_zeta

∀ (n : ℕ) [inst : NeZero n] (A : Type w) (B : Type z) [inst_1 : CommRing A] [inst_2 : CommRing B] [inst_3 : Algebra A B]
  [inst_4 : IsCyclotomicExtension {n} A B] [IsDomain B] [NeZero ↑n],
  (Polynomial.aeval (IsCyclotomicExtension.zeta n A B)) (Polynomial.cyclotomic n A) = 0

Defined in

Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots

Cited by

1 results in Mathlib

Foundations

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

Assumes

NeZeroCommRingCommRingAlgebraIsCyclotomicExtensionIsDomainNeZero