Commit 2022-01-13 12:25 cd4f5c40
View on Github →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