Def LinearMap.ltoFun

Modification history

2025-11-24 20:52

Mathlib/Algebra/Algebra/Basic.lean

chore: state `LinearMap.ltoFun` in the correct generality (#31952)

Modified LinearMap.ltoFun View on Github →

2023-02-19 01:12

Mathlib/Algebra/Algebra/Basic.lean

feat: port Algebra.Algebra.Basic (#2244)

Added LinearMap.ltoFun View on Github →