Commit 2024-01-31 15:04 0c4b7314

View on Github →

chore: golfing in categories of algebraic objects (#10114)

Estimated changes

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

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

modified def CategoryTheory.Iso.toLinearEquiv

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

modified def CategoryTheory.Iso.commRingCatIsoToRingEquiv

modified def CategoryTheory.Iso.ringCatIsoToRingEquiv

Modified Mathlib/CategoryTheory/Monoidal/Internal/Module.lean