Theorem Module.Finite_of_isLocalization

Modification history

2025-07-15 11:35
Mathlib/RingTheory/RingHom/Finite.lean
feat: add Mathlib.RingTheory.DedekindDomain.Instances (#26070) …
Deleted Module.Finite_of_isLocalizationView on Github →
2025-04-08 21:08
Mathlib/RingTheory/RingHom/Finite.lean
feat: generalize half of Mathlib.RingTheory (#23173) …
Modified Module.Finite_of_isLocalizationView on Github →
2024-09-24 15:04
Mathlib/RingTheory/LocalProperties.lean
chore(Mathlib/RingTheory/LocalProperties): split LocalProperties.lean (#16879) …
Modified Module.Finite_of_isLocalizationView on Github →
2024-01-09 09:24
Mathlib/RingTheory/LocalProperties.lean
feat: Define `intNorm` and `intTrace`. (#9265)
Added Module.Finite_of_isLocalizationView on Github →