Theorem Module.Finite_of_isLocalization

Modification history

2024-09-24 15:04

Mathlib/RingTheory/LocalProperties.lean

chore(Mathlib/RingTheory/LocalProperties): split LocalProperties.lean (#16879) …

Modified Module.Finite_of_isLocalization View on Github →

2024-01-09 09:24

Mathlib/RingTheory/LocalProperties.lean

feat: Define `intNorm` and `intTrace`. (#9265)

Added Module.Finite_of_isLocalization View on Github →