Commit 2025-11-24 20:52 3e37a71e

View on Github →

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

Estimated changes

Modified Mathlib/Algebra/Algebra/Basic.lean

deleted def LinearMap.ltoFun

Modified Mathlib/Algebra/Module/LinearMap/Basic.lean

added def LinearMap.ltoFun

added theorem LinearMap.ltoFun_apply

Modified Mathlib/Analysis/LocallyConvex/WeakDual.lean

Modified Mathlib/FieldTheory/Fixed.lean

Modified Mathlib/LinearAlgebra/LinearIndependent/Lemmas.lean