mathlib3
095c46c2 - feat(linear_algebra/basis): `reindex_refl` (#11626)

Commit

3 years ago

feat(linear_algebra/basis): `reindex_refl` (#11626) Add a `simp` lemma about applying `basis.reindex` with `equiv.refl`.

Author

jsm28

Parents