Theorem Algebra.EssFiniteType.isNoetherianRing

Modification history

2025-06-07 07:26

Mathlib/RingTheory/Localization/Submodule.lean

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

Added Algebra.EssFiniteType.isNoetherianRing View on Github →