Commit 2026-03-26 22:21 2f95960c

View on Github →

chore(LinearAlgebra/Matrix): generalize equivs and use where (#37178)

Generalize Matrix.compAddEquiv from AddCommMonoid to Add
Generalize Matrix.transposeRingEquiv from CommSemigroup to CommMagma
Generalize Matrix.conjTransposeRingEquiv from Semiring to NonUnitalNonAssocSemiring

Estimated changes

Modified Mathlib/Data/Matrix/Basic.lean

modified def Matrix.transposeRingEquiv

Modified Mathlib/Data/Matrix/Composition.lean

Modified Mathlib/LinearAlgebra/Matrix/ConjTranspose.lean

modified def Matrix.conjTransposeRingEquiv

Modified Mathlib/LinearAlgebra/Matrix/Reindex.lean

modified def Matrix.reindexAlgEquiv

modified def Matrix.reindexLinearEquiv