Commit 2024-11-04 21:50 3f3bba31

View on Github →

refactor(NumberTheory/RamificationInertia): use Ideal.LiesOver in some results about inertiaDeg (#18270) Use Ideal.LiesOver in the results about Ideal.inertiaDeg in the case [Algebra R S].

depends on: #18249

Estimated changes

Modified Mathlib/NumberTheory/RamificationInertia.lean

deleted theorem Ideal.Factors.inertiaDeg_ne_zero

modified theorem Ideal.FinrankQuotientMap.span_eq_top

modified theorem Ideal.inertiaDeg_algebraMap

added theorem Ideal.inertiaDeg_map_eq

added theorem Ideal.inertiaDeg_pos

added theorem Ideal.ramificationIdx_map_eq

Modified Mathlib/RingTheory/Ideal/Maps.lean

added theorem Ideal.map_comap_eq_self_of_equiv

Modified Mathlib/RingTheory/Ideal/Over.lean

added theorem Ideal.LiesOver.of_eq_comap

added theorem Ideal.LiesOver.of_eq_map_equiv

added def Ideal.Quotient.algEquivOfEqComap

added theorem Ideal.Quotient.algEquivOfEqComap_apply

added def Ideal.Quotient.algEquivOfEqMap

added theorem Ideal.Quotient.algEquivOfEqMap_apply

modified theorem Ideal.Quotient.algebraMap_injective_of_liesOver

added theorem Ideal.Quotient.nontrivial_of_liesOver_of_isPrime

added theorem Ideal.Quotient.nontrivial_of_liesOver_of_ne_top

added theorem Ideal.eq_top_iff_of_liesOver

Modified Mathlib/RingTheory/Localization/FractionRing.lean

added theorem NoZeroSMulDivisors.of_field_isFractionRing

added theorem algebraMap_injective_of_field_isFractionRing