Mathlib v3 is deprecated. Go to Mathlib v4

Def basis.map_coeffs

Modification history

2021-08-25 17:03
src/linear_algebra/basis.lean
feat(linear_algebra/basis): if `R ≃ R'`, map a basis for `R`-module `M` to `R'`-module `M` (#8699) …
Added basis.map_coeffsView on Github →