Commit 2025-11-10 19:42 28ac543f

View on Github →

feat(Algebra/Category): simp lemmas for Iso.toLinearEquiv (#31189) From ClassFieldTheory

Estimated changes

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

modified def CategoryTheory.Iso.toLinearEquiv

added theorem CategoryTheory.Iso.toLinearEquiv_apply

added theorem CategoryTheory.Iso.toLinearEquiv_symm

added theorem CategoryTheory.Iso.toLinearMap_toLinearEquiv