Mathlib v3 is deprecated. Go to Mathlib v4

Theorem basis.coe_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.coe_map_coeffsView on Github →