Commit 2023-05-23 10:39 d865f0cb

View on Github →

feat: port RingTheory.Localization.Integral (#4231)

Estimated changes

Modified Mathlib.lean

Created Mathlib/RingTheory/Localization/Integral.lean

added theorem IsFractionRing.comap_isAlgebraic_iff

added theorem IsFractionRing.ideal_span_singleton_map_subset

added theorem IsFractionRing.integerNormalization_eq_zero_iff

added theorem IsFractionRing.isAlgebraic_iff'

added theorem IsFractionRing.isAlgebraic_iff

added theorem IsIntegral.exists_multiple_integral_of_isLocalization

added theorem IsIntegralClosure.isFractionRing_of_algebraic

added theorem IsIntegralClosure.isFractionRing_of_finite_extension

added theorem IsLocalization.coeffIntegerNormalization_mem_support

added theorem IsLocalization.coeffIntegerNormalization_of_not_mem_support

added theorem IsLocalization.integerNormalization_aeval_eq_zero

added theorem IsLocalization.integerNormalization_coeff

added theorem IsLocalization.integerNormalization_eval₂_eq_zero

added theorem IsLocalization.integerNormalization_map_to_map

added theorem IsLocalization.integerNormalization_spec

added theorem IsLocalization.scaleRoots_commonDenom_mem_lifts

added theorem RingHom.isIntegralElem_localization_at_leadingCoeff

added theorem integralClosure.isFractionRing_of_algebraic

added theorem integralClosure.isFractionRing_of_finite_extension

added theorem isIntegral_localization'

added theorem isIntegral_localization

added theorem is_integral_localization_at_leadingCoeff