Commit 2026-10-28 13:41 e3f2f2dd

View on Github →

chore: make LinearMap.*_apply lemmas protected (#45319) This is preliminary work for using IsApply lemmas instead in #45307 and #45271 for instance.

Estimated changes

Modified Mathlib/Algebra/Exact/Basic.lean

Modified Mathlib/Algebra/FiveLemma.lean

Modified Mathlib/Algebra/Lie/Basic.lean

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

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

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

deleted theorem LinearMap.add_apply

deleted theorem LinearMap.neg_apply

deleted theorem LinearMap.smul_apply

deleted theorem LinearMap.sub_apply

deleted theorem LinearMap.zero_apply

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

Modified Mathlib/Algebra/Module/SnakeLemma.lean

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

deleted theorem LinearMap.sum_apply

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

Modified Mathlib/Analysis/InnerProductSpace/Positive.lean

Modified Mathlib/Analysis/InnerProductSpace/Symmetric.lean

Modified Mathlib/Analysis/LocallyConvex/Polar.lean

Modified Mathlib/Geometry/Convex/Cone/Dual.lean

Modified Mathlib/LinearAlgebra/BilinearForm/Properties.lean

Modified Mathlib/LinearAlgebra/BilinearMap.lean

Modified Mathlib/LinearAlgebra/Center.lean

Modified Mathlib/LinearAlgebra/Charpoly/Basic.lean

Modified Mathlib/LinearAlgebra/DFinsupp.lean

Modified Mathlib/LinearAlgebra/Dimension/DivisionRing.lean

Modified Mathlib/LinearAlgebra/Dual/Defs.lean

Modified Mathlib/LinearAlgebra/Dual/Lemmas.lean

Modified Mathlib/LinearAlgebra/Eigenspace/Zero.lean

Modified Mathlib/LinearAlgebra/Finsupp/LSum.lean

Modified Mathlib/LinearAlgebra/Pi.lean

Modified Mathlib/LinearAlgebra/Prod.lean

Modified Mathlib/LinearAlgebra/Projection.lean

Modified Mathlib/LinearAlgebra/QuadraticForm/Basic.lean

Modified Mathlib/LinearAlgebra/Quotient/Pi.lean

Modified Mathlib/LinearAlgebra/RootSystem/OfBilinear.lean

Modified Mathlib/LinearAlgebra/SesquilinearForm/Basic.lean

Modified Mathlib/LinearAlgebra/SesquilinearForm/Star.lean

Modified Mathlib/LinearAlgebra/TensorProduct/Map.lean

Modified Mathlib/LinearAlgebra/TensorProduct/Tower.lean

Modified Mathlib/LinearAlgebra/Trace.lean

Modified Mathlib/LinearAlgebra/Transvection/Basic.lean

Modified Mathlib/RepresentationTheory/Maschke.lean

Modified Mathlib/RingTheory/AdicCompletion/Functoriality.lean

Modified Mathlib/RingTheory/TensorProduct/Maps.lean

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