Commit 2026-04-27 15:18 2d59066e

View on Github →

refactor(Data/Matrix): protect Matrix.mul_smul (#38570) This avoids it conflicting with the more general SemigroupAction.mul_smul.

Estimated changes

Modified Mathlib/Algebra/Azumaya/Matrix.lean

Modified Mathlib/Data/Matrix/Mul.lean

deleted theorem Matrix.mul_smul

Modified Mathlib/GroupTheory/GroupAction/SubMulAction/OfStabilizer.lean

Modified Mathlib/LinearAlgebra/Eigenspace/Matrix.lean

Modified Mathlib/LinearAlgebra/FreeModule/Finite/Quotient.lean

Modified Mathlib/LinearAlgebra/Matrix/Adjugate.lean

Modified Mathlib/LinearAlgebra/Matrix/GeneralLinearGroup/FinTwo.lean

Modified Mathlib/LinearAlgebra/Matrix/Module.lean

Modified Mathlib/LinearAlgebra/Matrix/SemiringInverse.lean

Modified Mathlib/LinearAlgebra/Matrix/SesquilinearForm.lean

Modified Mathlib/LinearAlgebra/Matrix/ZPow.lean

Modified Mathlib/NumberTheory/ModularForms/BoundedAtCusp.lean

Modified Mathlib/NumberTheory/ModularForms/CongruenceSubgroups.lean

Modified Mathlib/NumberTheory/ModularForms/Cusps.lean

Modified Mathlib/RingTheory/Morita/Matrix.lean

Modified Mathlib/RingTheory/Trace/Basic.lean

Modified Mathlib/Topology/Compactification/OnePoint/ProjectiveLine.lean