Commit 2024-11-06 15:58 f20f26d7

View on Github →

refactor(RingTheory/Algebraic): Golf IsIntegralClosure.exists_smul_eq_mul (#18594) This PR golfs IsIntegralClosure.exists_smul_eq_mul by proving a generalization to algebraic extensions.

Estimated changes

Modified Mathlib/NumberTheory/ClassNumber/Finite.lean

modified theorem ClassGroup.exists_mem_finset_approx'

modified theorem ClassGroup.exists_mk0_eq_mk0

modified theorem ClassGroup.mkMMem_surjective

Modified Mathlib/NumberTheory/RamificationInertia.lean

Modified Mathlib/RingTheory/Algebraic.lean

added theorem Algebra.IsAlgebraic.exists_smul_eq_mul

added theorem IsAlgebraic.exists_nonzero_coeff_and_aeval_eq_zero

added theorem IsAlgebraic.exists_nonzero_dvd

added theorem IsAlgebraic.exists_smul_eq_mul

deleted theorem IsIntegralClosure.exists_smul_eq_mul

Modified Mathlib/RingTheory/Localization/Integral.lean