Theorem Ideal.exists_of_comap_eq_ker_sup

Modification history

2026-04-08 16:40
Mathlib/RingTheory/Ideal/Maps.lean
feat(RingTheory/Smooth): some lemmas about formally smooth (#35675) …
Added Ideal.exists_of_comap_eq_ker_supView on Github →