Commit 2024-11-07 05:22 92a5da5f
View on Github →feat(RingTheory/UFD): WfDvdMonoid.of_setOf_isPrincipal_wellFoundedOn_gt (#18422)
And the reverse Ideal.setOf_isPrincipal_wellFoundedOn_gt
the docstring for WfDvdMonoid mentioned the ACCP
but I didn't see the explicit result anywhere
I also used it to golf the Noetherian => WfDvdMonoid proof
And generalized to CommSemiring