Mathlib v3 is deprecated. Go to Mathlib v4

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

Estimated changes

added theorem matrix.smul_vec2
added theorem matrix.smul_vec3
added theorem matrix.vec2_add
added theorem matrix.vec2_eq
added theorem matrix.vec3_add
added theorem matrix.vec3_eq
added def cross.lie_ring
added theorem cross_anticomm'
added theorem cross_anticomm
added theorem cross_apply
added theorem cross_cross
added theorem cross_dot_cross
added def cross_product
added theorem cross_self
added theorem dot_cross_self
added theorem dot_self_cross
added theorem jacobi_cross
added theorem leibniz_cross
added theorem triple_product_eq_det