Commit 2026-10-29 16:29 5b08efb3

View on Github →

feat: use IsApply for LinearEquiv (#45391) I did not add an IsSMulApply instance because the already existing smul_apply lemma seems more relevant.

Estimated changes

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

deleted theorem LinearEquiv.mul_apply

deleted theorem LinearEquiv.pow_apply

deleted theorem LinearEquiv.zero_apply

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

deleted theorem LinearEquiv.smul_apply

Modified Mathlib/LinearAlgebra/FiniteSpan.lean

Modified Mathlib/LinearAlgebra/Reflection.lean

Modified Mathlib/LinearAlgebra/RootSystem/Defs.lean

Modified Mathlib/LinearAlgebra/Transvection/Generation.lean

Modified Mathlib/RingTheory/GradedAlgebra/Basic.lean

Modified Mathlib/RingTheory/GradedAlgebra/Homogeneous/Ideal.lean

Modified Mathlib/RingTheory/MvPolynomial/Homogeneous.lean