Commit 2026-08-03 08:56 53331279

View on Github →

chore: rename a lemma containing not_unit (#42387)

Estimated changes

Modified Mathlib/RingTheory/DiscreteValuationRing/TFAE.lean

Modified Mathlib/RingTheory/UniqueFactorizationDomain/Defs.lean

added theorem WfDvdMonoid.not_isUnit_iff_exists_factors_eq

deleted theorem WfDvdMonoid.not_unit_iff_exists_factors_eq