Commit 2024-07-26 21:05 30361bf1

View on Github →

feat: add SMul instances to Basis (#14945) Zulip thread for the naming clash.

Estimated changes

Modified Mathlib/LinearAlgebra/Basis.lean

added theorem Basis.coe_smul

added theorem Basis.repr_smul

added theorem Basis.smul_apply

added theorem Basis.smul_eq_map

Modified Mathlib/LinearAlgebra/Determinant.lean

added theorem Basis.smul_det

Modified Mathlib/LinearAlgebra/Matrix/Basis.lean

added theorem Basis.toMatrix_smul_left

Modified Mathlib/LinearAlgebra/Matrix/ToLin.lean

added theorem Algebra.smul_leftMulMatrix

added theorem LinearMap.toMatrix_smulBasis_left

added theorem LinearMap.toMatrix_smulBasis_right