Theorem Ideal.localized₀_eq_restrictScalars_map

Modification history

2024-11-26 20:08
Mathlib/RingTheory/LocalProperties/Basic.lean
chore(RingTheory/Localization): golfs and generalizations (#19310) …
Added Ideal.localized₀_eq_restrictScalars_mapView on Github →