Commit 2025-11-26 19:12 20a07479

View on Github →

chore: rename LinearMap.coeFn_sum to LinearMap.coe_sum (#32054)

Estimated changes

Modified Mathlib/Algebra/Azumaya/Matrix.lean

Modified Mathlib/Algebra/Lie/TraceForm.lean

Modified Mathlib/Algebra/Lie/Weights/Basic.lean

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

deleted theorem LinearMap.coeFn_sum

added theorem LinearMap.coe_sum

Modified Mathlib/LinearAlgebra/Basis/Defs.lean

Modified Mathlib/LinearAlgebra/BilinearForm/Hom.lean

Modified Mathlib/LinearAlgebra/BilinearForm/Properties.lean

Modified Mathlib/LinearAlgebra/Contraction.lean

Modified Mathlib/LinearAlgebra/Dual/Lemmas.lean

Modified Mathlib/LinearAlgebra/Eigenspace/Basic.lean

Modified Mathlib/LinearAlgebra/Matrix/SesquilinearForm.lean

Modified Mathlib/LinearAlgebra/Matrix/ToLin.lean

Modified Mathlib/LinearAlgebra/Multilinear/Basic.lean

Modified Mathlib/LinearAlgebra/RootSystem/Base.lean

Modified Mathlib/LinearAlgebra/RootSystem/Finite/CanonicalBilinear.lean

Modified Mathlib/LinearAlgebra/SesquilinearForm/Star.lean

Modified Mathlib/LinearAlgebra/TensorProduct/Pi.lean

Modified Mathlib/RingTheory/Bialgebra/MonoidAlgebra.lean

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

Modified Mathlib/Topology/Algebra/Module/ModuleTopology.lean