Theorem CategoryTheory.Iso.toLinearMap_toLinearEquiv

Modification history

2025-11-10 19:42
Mathlib/Algebra/Category/ModuleCat/Basic.lean
feat(Algebra/Category): simp lemmas for `Iso.toLinearEquiv` (#31189) …
Added CategoryTheory.Iso.toLinearMap_toLinearEquivView on Github →