Theorem UniqueFactorizationMonoid.iff_forall_isPrincipal_of_height_eq_one

Modification history

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