Mathlib v3 is deprecated. Go to Mathlib v4

Theorem basis.det_smul_mk_coord_eq_det_update

Modification history

2021-11-15 21:01
src/linear_algebra/determinant.lean
feat(linear_algebra/determinant): linear coordinates are ratio of determinants (#10261) …
Added basis.det_smul_mk_coord_eq_det_updateView on Github →