Commit 2024-11-15 19:36 ce8400c5

View on Github →

chore(Algebra/Category): remove a few erws (#19100)

Estimated changes

Modified Mathlib/Algebra/Category/AlgebraCat/Limits.lean

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

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

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

Modified Mathlib/Logic/Small/Group.lean

added theorem equivShrink_smul

added theorem equivShrink_symm_smul