Theorem WfDvdMonoid.of_setOf_isPrincipal_wellFoundedOn_gt

Modification history

2024-11-20 11:43

Mathlib/RingTheory/UniqueFactorizationDomain.lean

chore(RingTheory): split `UniqueFactorizationDomain.lean` (#19256) …

Modified WfDvdMonoid.of_setOf_isPrincipal_wellFoundedOn_gt View on Github →

2024-11-07 05:22

Mathlib/RingTheory/UniqueFactorizationDomain.lean

feat(RingTheory/UFD): `WfDvdMonoid.of_setOf_isPrincipal_wellFoundedOn_gt` (#18422) …

Added WfDvdMonoid.of_setOf_isPrincipal_wellFoundedOn_gt View on Github →