Commit 2026-02-15 14:33 c429693d

View on Github →

chore: rename "Punit" to "PUnit" in definitions (#34972) The previous names were simply wrong. Reported on zulip.

Estimated changes

Modified Mathlib/AlgebraicGeometry/Limits.lean

Modified Mathlib/CategoryTheory/Action/Basic.lean

added def Action.actionPUnitEquivalence

deleted def Action.actionPunitEquivalence

Modified Mathlib/CategoryTheory/Extensive.lean

Modified Mathlib/CategoryTheory/Limits/Sifted.lean

Modified Mathlib/CategoryTheory/Limits/Types/Products.lean

Modified Mathlib/Order/InitialSeg.lean

Modified Mathlib/RingTheory/FreeCommRing.lean

added def freeCommRingPUnitEquivPolynomialInt

deleted def freeCommRingPunitEquivPolynomialInt

added def freeRingPUnitEquivPolynomialInt

deleted def freeRingPunitEquivPolynomialInt

Modified Mathlib/Topology/UniformSpace/Equiv.lean

added def UniformEquiv.prodPUnit

deleted def UniformEquiv.prodPunit