Theorem Algebra.idealMap_eq_ofEq_comp_toLocalized₀

Modification history

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