Mathlib v3 is deprecated. Go to Mathlib v4

Theorem basis.mk_coord_apply_eq

Modification history

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_apply_eqView on Github →