Commit 2023-06-16 11:26 ee96c852

View on Github →

feat: port RingTheory.Polynomial.Cyclotomic.Roots (#5138)

Estimated changes

Modified Mathlib.lean

Created Mathlib/RingTheory/Polynomial/Cyclotomic/Roots.lean

added theorem IsPrimitiveRoot.isRoot_cyclotomic

added theorem IsPrimitiveRoot.minpoly_dvd_cyclotomic

added theorem IsPrimitiveRoot.minpoly_eq_cyclotomic_of_irreducible

added theorem Polynomial.cyclotomic.irreducible

added theorem Polynomial.cyclotomic.irreducible_rat

added theorem Polynomial.cyclotomic.isCoprime_rat

added theorem Polynomial.cyclotomic.roots_eq_primitiveRoots_val

added theorem Polynomial.cyclotomic.roots_to_finset_eq_primitiveRoots

added theorem Polynomial.cyclotomic_eq_minpoly

added theorem Polynomial.cyclotomic_eq_minpoly_rat

added theorem Polynomial.cyclotomic_injective

added theorem Polynomial.isRoot_cyclotomic_iff

added theorem Polynomial.isRoot_cyclotomic_iff_charZero

added theorem Polynomial.isRoot_of_unity_of_root_cyclotomic

added theorem Polynomial.roots_cyclotomic_nodup

added theorem isRoot_of_unity_iff