triple_product_eq_det
theorem triple_product_eq_det :
∀ {R : Type u_1} [inst : CommRing R] (u v w : Fin 3 → R),
Matrix.dotProduct u ((crossProduct v) w) = Matrix.det ![u, v, w]
The theorem `triple_product_eq_det` states that for any commutative ring `R` and any three vectors `u`, `v`, `w` in `R^3`, the dot product of `u` with the cross product of `v` and `w` is equal to the determinant of the matrix whose rows are the vectors `u`, `v`, and `w`. This is essentially a formalization of the geometric concept of the scalar triple product in the context of linear algebra and abstract algebra.
More concisely: For any commutative ring R and vectors u, v, w in R^3, the dot product of u with the cross product of v and w equals the determinant of the matrix having rows u, v, and w.
|
dot_self_cross
theorem dot_self_cross :
∀ {R : Type u_1} [inst : CommRing R] (v w : Fin 3 → R), Matrix.dotProduct v ((crossProduct v) w) = 0
This theorem states that for any commutative ring `R`, and any two vectors `v` and `w` from `R^3`, the dot product of vector `v` and the cross product of vectors `v` and `w` equals zero. In other words, the cross product of two vectors is always perpendicular to the first vector, as the dot product of two perpendicular vectors is zero.
More concisely: For any commutative ring `R` and vectors `v, w` in `R^3`, the dot product of `v` and the cross product of `v` and `w` is zero.
|
neg_cross
theorem neg_cross : ∀ {R : Type u_1} [inst : CommRing R] (v w : Fin 3 → R), -(crossProduct v) w = (crossProduct w) v
This theorem, referred to as the "neg_cross" theorem, states that for any commutative ring R with two vectors v and w in R³, the negative of the cross product of v with w is equal to the cross product of w with v. In mathematical terms, -(v × w) = w × v. This theorem essentially demonstrates the anti-commutative property of the cross product in a three-dimensional real space.
More concisely: The cross product of a vector with another vector is negated by exchanging the order of the vectors.
|
dot_cross_self
theorem dot_cross_self :
∀ {R : Type u_1} [inst : CommRing R] (v w : Fin 3 → R), Matrix.dotProduct w ((crossProduct v) w) = 0
This theorem states that for any two vectors `v` and `w` in three-dimensional space over a commutative ring `R`, the dot product of `w` and the cross product of `v` and `w` is zero. In other words, the vector obtained by taking the cross product of `v` and `w` is orthogonal (perpendicular) to the vector `w`, as their dot product is zero. This is an important property in linear algebra and vector calculus.
More concisely: For any vectors `v` and `w` in three-dimensional space over a commutative ring `R`, the dot product of `w` and the cross product of `v` and `w` equals zero.
|
cross_anticomm
theorem cross_anticomm :
∀ {R : Type u_1} [inst : CommRing R] (v w : Fin 3 → R), -(crossProduct v) w = (crossProduct w) v
The theorem `cross_anticomm` stipulates that for any commutative ring `R` and any two vectors `v` and `w` in `R^3`, the negative of the cross product of `v` and `w` is equal to the cross product of `w` and `v`. This essentially states that the cross product operation is anti-commutative, aligning with the known property in mathematics that the cross product of two vectors changes sign when the order of the vectors is switched.
More concisely: For any commutative ring R and vectors v, w in R^3, the cross product of v and w is equal to the negative of the cross product of w and v. In other words, the cross product is anti-commutative.
|
leibniz_cross
theorem leibniz_cross :
∀ {R : Type u_1} [inst : CommRing R] (u v w : Fin 3 → R),
(crossProduct u) ((crossProduct v) w) =
(crossProduct ((crossProduct u) v)) w + (crossProduct v) ((crossProduct u) w)
The theorem `leibniz_cross` states that for any commutative ring `R` and any three vectors `u`, `v`, `w` from `R^3`, the cross product operation satisfies the Leibniz property. In mathematical terms, this can be written as `(u × (v × w)) = ((u × v) × w) + (v × (u × w))`, where `×` denotes the cross product. This property is a key identity in the algebra of cross products.
More concisely: For any commutative ring R and vectors u, v, w in R^3, the cross product satisfies the Leibniz property: (u × (v × w)) = ((u × v) × w) + (v × (u × w)).
|
cross_dot_cross
theorem cross_dot_cross :
∀ {R : Type u_1} [inst : CommRing R] (u v w x : Fin 3 → R),
Matrix.dotProduct ((crossProduct u) v) ((crossProduct w) x) =
Matrix.dotProduct u w * Matrix.dotProduct v x - Matrix.dotProduct u x * Matrix.dotProduct v w
The theorem `cross_dot_cross` states an identity known as the scalar quadruple product identity, which is related to the Binet-Cauchy identity. This theorem applies in the context of a commutative ring `R`. Given four vectors `u`, `v`, `w`, and `x` in `R^3`, the dot product of the cross product of `u` with `v` and the cross product of `w` with `x`, is equal to the product of dot product of `u` with `w` and `v` with `x` minus the product of dot product of `u` with `x` and `v` with `w`. In mathematical terms, it says that `(u × v) . (w × x) = (u . w)(v . x) - (u . x)(v . w)`, where `×` denotes the cross product and `.` denotes the dot product.
More concisely: The scalar quadruple product identity in a commutative ring asserts that $(u \times v) \cdot (w \times x) = (u \cdot w)(v \cdot x) - (u \cdot x)(v \cdot w)$, where $\times$ denotes the cross product and $\cdot$ denotes the dot product.
|
triple_product_permutation
theorem triple_product_permutation :
∀ {R : Type u_1} [inst : CommRing R] (u v w : Fin 3 → R),
Matrix.dotProduct u ((crossProduct v) w) = Matrix.dotProduct v ((crossProduct w) u)
The theorem `triple_product_permutation` states that for any commutative ring `R` and any three vectors `u`, `v`, `w` in `R^3`, the cyclic permutations of vectors preserve the triple product. That is, the dot product of `u` and the cross product of `v` and `w` is equal to the dot product of `v` and the cross product of `w` and `u`. This can also be written in mathematical notation as u . (v × w) = v . (w × u). This is often related to the determinant of a 3x3 matrix consisting of the three vectors, as hinted by the comment `triple_product_eq_det`.
More concisely: The triple product of vectors u, v, and w in a commutative ring R, represented as the dot product of the first two vectors and the cross product of the last two, is commutative: u . (v × w) = v . (w × u).
|
jacobi_cross
theorem jacobi_cross :
∀ {R : Type u_1} [inst : CommRing R] (u v w : Fin 3 → R),
(crossProduct u) ((crossProduct v) w) + (crossProduct v) ((crossProduct w) u) +
(crossProduct w) ((crossProduct u) v) =
0
The theorem, often referred to as the "Jacobi identity", asserts that for any three vectors in a 3-dimensional space over a commutative ring, the sum of the cross products of these vectors taken in any of the three even permutations is equal to the zero vector. In other words, for any vectors `u`, `v`, and `w` in `R^3`, where `R` is a commutative ring, the following equation holds: `(crossProduct u) ((crossProduct v) w) + (crossProduct v) ((crossProduct w) u) + (crossProduct w) ((crossProduct u) v) = 0`. This identity is a fundamental property in the algebra of cross products.
More concisely: For any vectors `u`, `v`, and `w` in a 3-dimensional space over a commutative ring, the sum of the cross products of these vectors in any two opposite orders is equal to the negative of the cross product of the third vector with the vector obtained by cyclically permuting the first two. That is, `(crossProduct u (crossProduct v w)) + (crossProduct v (crossProduct w u)) = -(crossProduct w (crossProduct u v))`.
|