Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-02-28 10:33 e700d561

View on Github →

feat(ring_theory/polynomial/eisenstein): add a technical lemma (#11839) A technical lemma about Eiseinstein minimal polynomials. From flt-regular

Estimated changes

Modified src/algebra/associated.lean

added theorem prime.dvd_of_pow_dvd_pow_mul_pow_of_square_not_dvd

Modified src/data/nat/basic.lean

added theorem nat.le_add_pred_of_pos

Modified src/data/polynomial/monic.lean

added theorem polynomial.degree_map_of_monic

added theorem polynomial.nat_degree_map_of_monic

Modified src/ring_theory/integral_closure.lean

added theorem is_integral_smul

Modified src/ring_theory/polynomial/eisenstein.lean

added theorem dvd_coeff_zero_of_aeval_eq_prime_smul_of_minpoly_is_eiseinstein_at