Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-07-16 11:29 511a9f79

View on Github →

feat(algebra/gcd_monoid): GCD domains are integrally closed. (#15109)

Estimated changes

Modified src/algebra/gcd_monoid/basic.lean

added theorem extract_gcd

added theorem is_unit_gcd_of_eq_mul_gcd

Created src/algebra/gcd_monoid/integrally_closed.lean

added theorem is_localization.surj_of_gcd_domain

Modified src/ring_theory/polynomial/eisenstein.lean

added theorem polynomial.dvd_pow_nat_degree_of_aeval_eq_zero

added theorem polynomial.dvd_pow_nat_degree_of_eval₂_eq_zero

added theorem polynomial.scale_roots.is_weakly_eisenstein_at

Modified src/ring_theory/polynomial/scale_roots.lean

deleted theorem coeff_scale_roots

deleted theorem coeff_scale_roots_nat_degree

deleted theorem degree_scale_roots

deleted theorem monic_scale_roots_iff

deleted theorem nat_degree_scale_roots

added theorem polynomial.coeff_scale_roots

added theorem polynomial.coeff_scale_roots_nat_degree

added theorem polynomial.degree_scale_roots

added theorem polynomial.monic_scale_roots_iff

added theorem polynomial.nat_degree_scale_roots

added theorem polynomial.scale_roots_aeval_eq_zero

added theorem polynomial.scale_roots_aeval_eq_zero_of_aeval_div_eq_zero

added theorem polynomial.scale_roots_eval₂_eq_zero

added theorem polynomial.scale_roots_eval₂_eq_zero_of_eval₂_div_eq_zero

added theorem polynomial.scale_roots_ne_zero

added theorem polynomial.support_scale_roots_eq

added theorem polynomial.support_scale_roots_le

added theorem polynomial.zero_scale_roots

deleted theorem scale_roots_aeval_eq_zero

deleted theorem scale_roots_aeval_eq_zero_of_aeval_div_eq_zero

deleted theorem scale_roots_eval₂_eq_zero

deleted theorem scale_roots_eval₂_eq_zero_of_eval₂_div_eq_zero

deleted theorem scale_roots_ne_zero

deleted theorem support_scale_roots_eq

deleted theorem support_scale_roots_le

deleted theorem zero_scale_roots