Mathlib v3 is deprecated. Go to Mathlib v4

Theorem basis.mk_coord_apply

Modification history

2023-01-22 01:07
src/linear_algebra/basis.lean
fix(linear_algebra/basis): add missing decidable arguments in lemmas (#18252) …
Modified basis.mk_coord_applyView on Github →
2021-11-15 21:01
src/linear_algebra/basis.lean
feat(linear_algebra/determinant): linear coordinates are ratio of determinants (#10261) …
Added basis.mk_coord_applyView on Github →