Mathlib v3 is deprecated. Go to Mathlib v4

Theorem basis.coe_algebra_map_coeffs

Modification history

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