Commit 2023-09-12 17:41 198327e1

View on Github →

chore(Order/RelIso): golf, fix NS (#7114)

Rename Surjective.wellFounded_iff to Function.Surjective.wellFounded_iff.
Golf the proof.

Estimated changes

Modified Mathlib/Order/RelIso/Basic.lean

added theorem Function.Surjective.wellFounded_iff

deleted theorem Surjective.wellFounded_iff

Modified Mathlib/RingTheory/UniqueFactorizationDomain.lean

modified theorem WfDvdMonoid.of_wfDvdMonoid_associates

Modified Mathlib/Topology/NoetherianSpace.lean