Mathlib Map

Theorems · Theorem · number theory

Polynomial.cyclotomic.irreducible

∀ {n : ℕ}, 0 < n → Irreducible (Polynomial.cyclotomic n ℤ)

cyclotomic n ℤ is irreducible.

Defined in
Mathlib.RingTheory.Polynomial.Cyclotomic.Roots
Cited by
1 results in Mathlib
Foundations
Depth 209 from the axioms · uses propext, Classical.choice, Quot.sound
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Polynomial.cyclotomic.irreducible_rat · cited by 18cyclotomic.irreducible_ratPolynomial · cited by 5681PolynomialLT.lt.ne' · cited by 1417lt.ne'Irreducible · cited by 496IrreduciblePolynomial.cyclotomic · cited by 130Polynomial.cyclotomicminpoly.irreducible · cited by 26minpoly.irreducibleIsPrimitiveRoot.isIntegral · cited by 15IsPrimitiveRoot.isIntegralComplex.isPrimitiveRoot_exp · cited by 14Complex.isPrimitiveRoot_e…Polynomial.cyclotomic_eq_minpoly · cited by 7Polynomial.cyclotomic_eq_…cyclotomic.irreducibleCITED BYCITES

Cites8

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Cited by1

Results whose statement or proof uses this declaration.