Mathlib v3 is deprecated. Go to Mathlib v4

Theorem basis.algebra_map_coeffs_apply

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.algebra_map_coeffs_applyView on Github →