Commit 2024-06-29 09:06 3321494a

View on Github →

chore: reduce imports on the path to LinearMap (#14246)

Estimated changes

Modified Mathlib.lean

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

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

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

deleted def MulSemiringAction.toRingEquiv

Created Mathlib/Algebra/Ring/Action/Group.lean

added def MulSemiringAction.toRingEquiv

Modified Mathlib/Algebra/Ring/Aut.lean

Modified Mathlib/Algebra/Ring/BooleanRing.lean

Modified Mathlib/CategoryTheory/SingleObj.lean

Modified Mathlib/GroupTheory/GroupAction/Hom.lean

Modified scripts/noshake.json