Commit 2025-06-07 07:26 8ee00f5b

View on Github →

feat: connection between Algebra.IsUnramifiedAt and Ideal.ramificationIdx. (#25498)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/NumberTheory/RamificationInertia/Basic.lean

added theorem Ideal.IsDedekindDomain.ramificationIdx_eq_one_iff

added theorem Ideal.ramificationIdx_eq_one_of_map_localization

added theorem Ideal.ramificationIdx_ne_one_iff

Created Mathlib/NumberTheory/RamificationInertia/Unramified.lean

added theorem Algebra.IsUnramifiedAt.of_liesOver

added theorem Algebra.isUnramifiedAt_iff_of_isDedekindDomain

added theorem Ideal.ramificationIdx_eq_one_of_isUnramifiedAt

added theorem IsUnramifiedAt.of_liesOver_of_ne_bot

Created Mathlib/RingTheory/LocalRing/ResidueField/Algebraic.lean

Modified Mathlib/RingTheory/LocalRing/ResidueField/Ideal.lean

Modified Mathlib/RingTheory/Localization/AtPrime.lean

Modified Mathlib/RingTheory/Localization/Basic.lean

Modified Mathlib/RingTheory/Localization/Submodule.lean

added theorem Algebra.EssFiniteType.isNoetherianRing

Modified Mathlib/RingTheory/Unramified/LocalRing.lean

Modified Mathlib/RingTheory/Unramified/Locus.lean

added theorem Algebra.IsUnramifiedAt.comp

added theorem Algebra.IsUnramifiedAt.of_restrictScalars