Def LinearMap.evalAddMonoidHom
Modification history
2024-07-01 08:42
Mathlib/Algebra/Module/LinearMap/Basic.lean
chore(Algebra/Module/LinearMap): split into Basic and Defs (#14226) …
Modified LinearMap.evalAddMonoidHomView on Github →2024-04-22 09:41
Mathlib/Algebra/Module/LinearMap/Basic.lean
chore: redistribute a few results from Algebra.Module.Submodule.LinearMap (#12295) …
Modified LinearMap.evalAddMonoidHomView on Github →2023-11-15 16:58
Mathlib/Algebra/Module/Submodule/LinearMap.lean
chore: redistribute some of the results in LinearAlgebra.Basic (#7801) …
Modified LinearMap.evalAddMonoidHomView on Github →