Commit 2026-08-06 01:28 bf6473c6

View on Github →

chore: rename some lemmas containing not_unit (#42386)

Estimated changes

Modified Mathlib/Algebra/Prime/Lemmas.lean

added theorem DvdNotUnit.not_isUnit

deleted theorem DvdNotUnit.not_unit

added theorem not_irreducible_of_not_isUnit_of_dvdNotUnit

deleted theorem not_irreducible_of_not_unit_dvdNotUnit

Modified Mathlib/RingTheory/ChainOfDivisors.lean