Theorem Ideal.le_of_map_algebraMap_le

Modification history

2026-06-29 08:56
Mathlib/RingTheory/Localization/Away/Lemmas.lean
feat(RingTheory): UFD criteria via height `1` prime ideals and localization (#36739) …
Added Ideal.le_of_map_algebraMap_leView on Github →