Theorem IsLocalization.integerNormalization_support

Modification history

2026-03-02 23:05

Mathlib/RingTheory/Localization/Integral.lean

refactor(RingTheory/Localization/Integral): Simplify `integerNormalization` (#34877) …

Added IsLocalization.integerNormalization_support View on Github →