Commit 2023-06-16 09:03 474faf13

View on Github →

feat: port RingTheory.RootsOfUnity.Minpoly (#5119)

depends on: #5076

Estimated changes

Modified Mathlib.lean

Created Mathlib/RingTheory/RootsOfUnity/Minpoly.lean

added theorem IsPrimitiveRoot.isIntegral

added theorem IsPrimitiveRoot.is_roots_of_minpoly

added theorem IsPrimitiveRoot.minpoly_dvd_expand

added theorem IsPrimitiveRoot.minpoly_dvd_mod_p

added theorem IsPrimitiveRoot.minpoly_dvd_pow_mod

added theorem IsPrimitiveRoot.minpoly_dvd_x_pow_sub_one

added theorem IsPrimitiveRoot.minpoly_eq_pow

added theorem IsPrimitiveRoot.minpoly_eq_pow_coprime

added theorem IsPrimitiveRoot.pow_isRoot_minpoly

added theorem IsPrimitiveRoot.separable_minpoly_mod

added theorem IsPrimitiveRoot.squarefree_minpoly_mod

added theorem IsPrimitiveRoot.totient_le_degree_minpoly