Theorem Matrix.toEquiv_reindexRingEquiv

Modification history

2026-06-06 21:53

Mathlib/LinearAlgebra/Matrix/Reindex.lean

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

Added Matrix.toEquiv_reindexRingEquiv View on Github →