mathlib
36d3b688 - feat(linear_algebra/basis): `basis.map_equiv_fun` (#11888)

Commit

3 years ago

feat(linear_algebra/basis): `basis.map_equiv_fun` (#11888) Add a `simp` lemma about the effect of `equiv_fun` for a basis obtained with `basis.map`.

Author

jsm28

Parents