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_coeffs View on Github →