Theorem CategoryTheory.Iso.toLinearEquiv_apply

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.toLinearEquiv_applyView on Github →