Commit 2026-10-29 17:20 c5e59a9d

View on Github →

feat: use IsApply for Module.Basis (#45307)

Estimated changes

Modified Mathlib/LinearAlgebra/Basis/SMul.lean

modified theorem Module.Basis.coe_smul

deleted theorem Module.Basis.smul_apply

Modified Mathlib/LinearAlgebra/Matrix/ToLin.lean