mathlib3

cd4f5c40 - feat(linear_algebra/{cross_product,vectors}): cross product (#11181)

feat(linear_algebra/{cross_product,vectors}): cross product (#11181) Defines the cross product for R^3 and gives localized notation for that and the dot product. Was https://github.com/leanprover-community/mathlib/pull/10959 Co-authored-by: Kyle Miller <kmill31415@gmail.com> Co-authored-by: Eric Wieser <wieser.eric@gmail.com> Co-authored-by: Martin Dvořák <martin.dvorak@matfyz.cz>