Theorem Matrix.coe_reindexLinearEquiv

Modification history

2026-06-06 21:53

Mathlib/LinearAlgebra/Matrix/Reindex.lean

feat(LinearAlgebra/Matrix): `reindex` as `AddEquiv` and `RingEquiv` (#39106) …

Added Matrix.coe_reindexLinearEquiv View on Github →