Commit 2026-02-10 16:30 1932ef24

View on Github →

chore: rename "Pempty" to "PEmpty" in two definitions (#34971) The previous names were simply wrong. Reported on zulip.

Estimated changes

Modified Mathlib/RingTheory/FreeCommRing.lean

added def freeCommRingPEmptyEquivInt

deleted def freeCommRingPemptyEquivInt

added def freeRingPEmptyEquivInt

deleted def freeRingPemptyEquivInt