Commit 2026-10-26 17:38 2b2e9674

View on Github →

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

Estimated changes

Modified Mathlib/Algebra/Azumaya/Matrix.lean

Modified Mathlib/Algebra/Lie/Classical.lean

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

Modified Mathlib/Analysis/Complex/UpperHalfPlane/MoebiusAction.lean

Modified Mathlib/Analysis/Convex/Birkhoff.lean

Modified Mathlib/Analysis/InnerProductSpace/GramMatrix.lean

Modified Mathlib/Combinatorics/SimpleGraph/AdjMatrix.lean

Modified Mathlib/Combinatorics/SimpleGraph/IncMatrix.lean

Modified Mathlib/Data/Matrix/Basic.lean

deleted theorem Matrix.sum_apply

Modified Mathlib/Data/Matrix/Basis.lean

Modified Mathlib/Data/Matrix/Block.lean

Modified Mathlib/Data/Matrix/ColumnRowPartitioned.lean

Modified Mathlib/Data/Matrix/Composition.lean

Modified Mathlib/Data/Matrix/Diagonal.lean

deleted theorem Matrix.intCast_apply

deleted theorem Matrix.natCast_apply

deleted theorem Matrix.one_apply

Modified Mathlib/Data/Matrix/Mul.lean

deleted theorem Matrix.mul_apply

Modified Mathlib/Data/Matrix/PEquiv.lean

Modified Mathlib/LinearAlgebra/Matrix/AbsoluteValue.lean

Modified Mathlib/LinearAlgebra/Matrix/Adjugate.lean

Modified Mathlib/LinearAlgebra/Matrix/Block.lean

Modified Mathlib/LinearAlgebra/Matrix/CharP.lean

Modified Mathlib/LinearAlgebra/Matrix/Charpoly/Basic.lean

Modified Mathlib/LinearAlgebra/Matrix/Charpoly/Coeff.lean

Modified Mathlib/LinearAlgebra/Matrix/Charpoly/Univ.lean

Modified Mathlib/LinearAlgebra/Matrix/Circulant.lean

Modified Mathlib/LinearAlgebra/Matrix/ConjTranspose.lean

Modified Mathlib/LinearAlgebra/Matrix/Defs.lean

deleted theorem Matrix.add_apply

deleted theorem Matrix.neg_apply

deleted theorem Matrix.smul_apply

deleted theorem Matrix.sub_apply

deleted theorem Matrix.zero_apply

Modified Mathlib/LinearAlgebra/Matrix/Determinant/Basic.lean

Modified Mathlib/LinearAlgebra/Matrix/Determinant/TotallyUnimodular.lean

Modified Mathlib/LinearAlgebra/Matrix/DualNumber.lean

Modified Mathlib/LinearAlgebra/Matrix/HadamardMatrix.lean

Modified Mathlib/LinearAlgebra/Matrix/Ideal.lean

Modified Mathlib/LinearAlgebra/Matrix/Integer.lean

Modified Mathlib/LinearAlgebra/Matrix/InvariantBasisNumber.lean

Modified Mathlib/LinearAlgebra/Matrix/Irreducible/Defs.lean

Modified Mathlib/LinearAlgebra/Matrix/Kronecker.lean

Modified Mathlib/LinearAlgebra/Matrix/Module.lean

Modified Mathlib/LinearAlgebra/Matrix/Permanent.lean

Modified Mathlib/LinearAlgebra/Matrix/PosDef.lean

Modified Mathlib/LinearAlgebra/Matrix/Rank.lean

Modified Mathlib/LinearAlgebra/Matrix/RowCol.lean

Modified Mathlib/LinearAlgebra/Matrix/SemiringInverse.lean

Modified Mathlib/LinearAlgebra/Matrix/Trace.lean

Modified Mathlib/LinearAlgebra/Matrix/Transvection.lean

Modified Mathlib/LinearAlgebra/Matrix/Unique.lean

Modified Mathlib/LinearAlgebra/Matrix/Vec.lean

Modified Mathlib/LinearAlgebra/RootSystem/GeckConstruction/Semisimple.lean

Modified Mathlib/LinearAlgebra/UnitaryGroup.lean

Modified Mathlib/RingTheory/Morita/Matrix.lean