Commit 2025-02-11 11:19 9a88a779

View on Github →

chore(Algebra/PUnitInstances): sort files according to topic (#21045) Being about PUnit isn't really a topic. Let's follow the existing convention that Foo instances about Bar are in Algebra.Foo.Bar.

Estimated changes

Modified Counterexamples/CharPZeroNeCharZero.lean

Modified Mathlib.lean

Modified Mathlib/Algebra/Category/GrpWithZero.lean

Modified Mathlib/Algebra/Category/ModuleCat/Basic.lean

Modified Mathlib/Algebra/Category/MonCat/Basic.lean

Modified Mathlib/Algebra/Category/MonCat/Colimits.lean

Modified Mathlib/Algebra/Category/MonCat/ForgetCorepresentable.lean

Modified Mathlib/Algebra/Category/Ring/Basic.lean

Renamed Mathlib/Algebra/PUnitInstances/GCDMonoid.lean to Mathlib/Algebra/GCDMonoid/PUnit.lean

Renamed Mathlib/Algebra/PUnitInstances/Algebra.lean to Mathlib/Algebra/Group/PUnit.lean

modified theorem PUnit.div_eq

modified theorem PUnit.inv_eq

modified theorem PUnit.mul_eq

modified theorem PUnit.one_eq

Renamed Mathlib/Algebra/PUnitInstances/Module.lean to Mathlib/Algebra/Module/PUnit.lean

Modified Mathlib/Algebra/Module/Submodule/Lattice.lean

Renamed Mathlib/Algebra/PUnitInstances/Order.lean to Mathlib/Algebra/Order/PUnit.lean

Modified Mathlib/Algebra/Ring/BooleanRing.lean

Created Mathlib/Algebra/Ring/PUnit.lean

Modified Mathlib/Analysis/Normed/Group/Constructions.lean

Modified Mathlib/CategoryTheory/Action/Basic.lean

Modified Mathlib/CategoryTheory/Category/Grpd.lean

Modified Mathlib/CategoryTheory/Limits/Shapes/SingleObj.lean

Modified Mathlib/CategoryTheory/Monoidal/Internal/Types/Basic.lean

Modified Mathlib/CategoryTheory/Monoidal/Mon_.lean

Modified Mathlib/CategoryTheory/SingleObj.lean

Modified Mathlib/GroupTheory/Coprod/Basic.lean