Theorem Matrix.reindexRingEquiv_refl

Modification history

2026-06-06 21:53

Mathlib/LinearAlgebra/Matrix/Reindex.lean

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

Added Matrix.reindexRingEquiv_refl View on Github →