Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-09-09 07:32 f6ccb6b8

View on Github →

chore(ring_theory/polynomial/cyclotomic): golf+remove nontrivial (#9090)

Estimated changes

Modified src/ring_theory/polynomial/cyclotomic.lean

deleted theorem cyclotomic.irreducible

deleted theorem cyclotomic_eq_minpoly

deleted theorem minpoly_primitive_root_dvd_cyclotomic

added theorem polynomial.cyclotomic.irreducible

modified theorem polynomial.cyclotomic_eq_X_pow_sub_one_div

modified theorem polynomial.cyclotomic_eq_geom_sum

added theorem polynomial.cyclotomic_eq_minpoly

modified theorem polynomial.eq_cyclotomic_iff

added theorem polynomial.int_coeff_of_cyclotomic'

deleted theorem polynomial.int_coeff_of_cyclotomic

added theorem polynomial.minpoly_primitive_root_dvd_cyclotomic