Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2023-01-23 08:58 2032a878

View on Github →

chore(field_theory/minpoly/*): replace gcd_monoid.lean by is_integrally_closed.lean and remove results that have been generalized (#18206)

Estimated changes

Modified src/algebra/gcd_monoid/integrally_closed.lean

Modified src/field_theory/minpoly/default.lean

Renamed src/field_theory/minpoly/gcd_monoid.lean to src/field_theory/minpoly/is_integrally_closed.lean

deleted theorem minpoly.gcd_domain_dvd

deleted theorem minpoly.gcd_domain_eq_field_fractions'

deleted theorem minpoly.gcd_domain_eq_field_fractions

modified theorem minpoly.is_integrally_closed_dvd

added theorem minpoly.is_integrally_closed_dvd_iff

deleted theorem minpoly.is_integrally_closed_eq_field_fractions''

Modified src/number_theory/cyclotomic/discriminant.lean

Modified src/number_theory/cyclotomic/rat.lean

Modified src/number_theory/number_field/embeddings.lean

Modified src/ring_theory/dedekind_domain/adic_valuation.lean

Modified src/ring_theory/dedekind_domain/selmer_group.lean

Modified src/ring_theory/is_adjoin_root.lean

modified theorem is_adjoin_root_monic.minpoly_eq

Modified src/ring_theory/polynomial/cyclotomic/basic.lean

Created src/ring_theory/polynomial/eisenstein/basic.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.is_eisenstein_at.coeff_mem

added theorem polynomial.is_eisenstein_at.irreducible

added theorem polynomial.is_eisenstein_at.is_weakly_eisenstein_at

added structure polynomial.is_eisenstein_at

added theorem polynomial.is_weakly_eisenstein_at.exists_mem_adjoin_mul_eq_pow_nat_degree

added theorem polynomial.is_weakly_eisenstein_at.exists_mem_adjoin_mul_eq_pow_nat_degree_le

added theorem polynomial.is_weakly_eisenstein_at.map

added theorem polynomial.is_weakly_eisenstein_at.pow_nat_degree_le_of_aeval_zero_of_monic_mem_map

added theorem polynomial.is_weakly_eisenstein_at.pow_nat_degree_le_of_root_of_monic_mem

added structure polynomial.is_weakly_eisenstein_at

added theorem polynomial.monic.is_eisenstein_at_of_mem_of_not_mem

added theorem polynomial.monic.leading_coeff_not_mem

added theorem polynomial.scale_roots.is_weakly_eisenstein_at

Renamed src/ring_theory/polynomial/eisenstein.lean to src/ring_theory/polynomial/eisenstein/is_integral.lean

deleted theorem polynomial.dvd_pow_nat_degree_of_aeval_eq_zero

deleted theorem polynomial.dvd_pow_nat_degree_of_eval₂_eq_zero

deleted theorem polynomial.is_eisenstein_at.coeff_mem

deleted theorem polynomial.is_eisenstein_at.irreducible

deleted theorem polynomial.is_eisenstein_at.is_weakly_eisenstein_at

deleted structure polynomial.is_eisenstein_at

deleted theorem polynomial.is_weakly_eisenstein_at.exists_mem_adjoin_mul_eq_pow_nat_degree

deleted theorem polynomial.is_weakly_eisenstein_at.exists_mem_adjoin_mul_eq_pow_nat_degree_le

deleted theorem polynomial.is_weakly_eisenstein_at.map

deleted theorem polynomial.is_weakly_eisenstein_at.pow_nat_degree_le_of_aeval_zero_of_monic_mem_map

deleted theorem polynomial.is_weakly_eisenstein_at.pow_nat_degree_le_of_root_of_monic_mem

deleted structure polynomial.is_weakly_eisenstein_at

deleted theorem polynomial.monic.is_eisenstein_at_of_mem_of_not_mem

deleted theorem polynomial.monic.leading_coeff_not_mem

deleted theorem polynomial.scale_roots.is_weakly_eisenstein_at

Modified src/ring_theory/roots_of_unity.lean

modified theorem is_primitive_root.minpoly_dvd_expand