Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-03-08 14:29 c0ba4d69

View on Github →

feat(ring_theory/polynomial/eisenstein): add cyclotomic_comp_X_add_one_is_eisenstein_at (#12447) We add cyclotomic_comp_X_add_one_is_eisenstein_at: (cyclotomic p ℤ).comp (X + 1) is Eisenstein at p. From flt-regular

Estimated changes

Modified src/data/polynomial/coeff.lean

added theorem polynomial.mul_X_injective

added theorem polynomial.mul_X_pow_injective

Modified src/field_theory/minpoly.lean

added theorem minpoly.add_algebra_map

deleted theorem minpoly.minpoly_add_algebra_map

deleted theorem minpoly.minpoly_sub_algebra_map

added theorem minpoly.sub_algebra_map

Modified src/number_theory/cyclotomic/primitive_roots.lean

added theorem is_primitive_root.minpoly_sub_one_eq_cyclotomic_comp

Modified src/ring_theory/polynomial/basic.lean

added theorem polynomial.geom_sum_X_comp_X_add_one_eq_sum

added theorem polynomial.monic.geom_sum'

added theorem polynomial.monic.geom_sum

added theorem polynomial.monic_geom_sum_X

Modified src/ring_theory/polynomial/eisenstein.lean

added theorem cyclotomic_comp_X_add_one_is_eisenstein_at