Theorem IsLocalization.height_comap

Modification history

2026-05-12 12:43
Mathlib/RingTheory/Ideal/Height.lean
chore(RingTheory/Localization/AtPrime/Basic): use `under` instead of `comap (algebraMap R S)` (#37840) …
Deleted IsLocalization.height_comapView on Github →
2025-03-13 07:17
Mathlib/RingTheory/Ideal/Height.lean
feat(RingTheory/Ideal): more lemmas about the height of an ideal (#21041) …
Added IsLocalization.height_comapView on Github →