Commit 2025-02-14 12:41 60664e39

View on Github →

chore(RingTheory/MatrixAlgebra): reorder type arguments (#21863) Putting the index type first is consistent with Matrix (and its API like Matrix.transposeRingEquiv) and Basis.

Estimated changes

Modified Mathlib/RingTheory/MatrixAlgebra.lean

modified theorem MatrixEquivTensor.invFun_algebraMap

modified theorem MatrixEquivTensor.invFun_zero

modified theorem MatrixEquivTensor.left_inv

modified theorem MatrixEquivTensor.right_inv

Modified Mathlib/RingTheory/PolynomialAlgebra.lean