Revision #1171 → #1974 · back to history
modifiedDot product in three dimensions012aab46d255
| Field | From #1171 | To #1974 |
|---|
| mathlib.module | Mathlib.Data.Matrix.Mul | Mathlib.LinearAlgebra.Matrix.Notation |
| note | The 3D case isn't a standalone declaration but follows by `vec3_dotProduct`/`Matrix.dotProduct` on `Fin 3 → R`. | `Matrix.vec3_dotProduct` unfolds the dot product on `Fin 3 → R` to the explicit three-term sum. |
modifiedDot product as matrix product92d7761ab6f4
| Field | From #1171 | To #1974 |
|---|
| note | Mathlib expresses this via `Matrix.mul_apply`/`mulVec`/`vecMul` which unfold to `dotProduct`, but there is no dedicated row-times-column identity for dot product. | `Matrix.mul_apply` defines `(A * B) i j = ∑ k, A i k * B k j`, so a 1×n by n×1 product unfolds to `dotProduct`, but no dedicated row-times-column identity is named. |
modifiedOrthogonal and codirectional cases91835e3c9c57
| Field | From #1171 | To #1974 |
|---|
| mathlib.decl | inner_eq_zero_iff | Submodule.mem_orthogonal_singleton_iff_inner_right |
| mathlib.module | Mathlib.Analysis.InnerProductSpace.Basic | Mathlib.Analysis.InnerProductSpace.Orthogonal |
| note | The perpendicular case is captured by `inner_eq_zero_iff`/`orthogonal`; the codirectional/antidirectional cases are not stated as such but are direct consequences. | The perpendicular case is captured via `Submodule.mem_orthogonal_singleton_iff_inner_right`/`inner_eq_zero_symm`; the codirectional/antidirectional cases are not stated as such but follow from `cos_angle_mul_norm_mul_norm`. |
addedEuclidean length from self dot producte224618f1273
modifiedScalar projection8347d9e506d3
| Field | From #1171 | To #1974 |
|---|
| mathlib.decl | orthogonalProjection | Submodule.orthogonalProjectionOnto |
| note | Mathlib has `orthogonalProjection` (the vector projection) but no named scalar projection `‖a‖ cos θ`. | Mathlib has `Submodule.orthogonalProjectionOnto` (the vector projection) but no named scalar projection `‖a‖ cos θ`. |
modifiedHomogeneity and distributivityc8c94f0ada2f
| Field | From #1171 | To #1974 |
|---|
| note | `add_dotProduct`, `dotProduct_add`, `smul_dotProduct`, `dotProduct_smul` (and corresponding inner-product lemmas) give bilinearity. | `Matrix.add_dotProduct`, `dotProduct_add`, `smul_dotProduct`, `dotProduct_smul` (and corresponding inner-product lemmas) give bilinearity. |
modifiedStandard basis orthonormality and Kronecker delta3d3e1f92fc60
| Field | From #1171 | To #1974 |
|---|
| note | `EuclideanSpace.basisFun` is an `OrthonormalBasis` and `EuclideanSpace.inner_single_left` evaluates the Kronecker-delta inner product. | `EuclideanSpace.basisFun` is the standard `OrthonormalBasis` and `EuclideanSpace.inner_single_left` evaluates the Kronecker-delta inner product. |
addedCommutativity of the real dot product44c1ed45fbb3
modifiedAssociativity with scalar multiplication6175746c1f03
| Field | From #1171 | To #1974 |
|---|
| note | `smul_dotProduct` and `dotProduct_smul` give `(c • v) ⬝ᵥ w = c • (v ⬝ᵥ w)`. | `Matrix.smul_dotProduct` and `Matrix.dotProduct_smul` give `(c • v) ⬝ᵥ w = c • (v ⬝ᵥ w)`. |
modifiedOrthogonality criterion5b6a82b58730
| Field | From #1171 | To #1974 |
|---|
| mathlib.decl | inner_eq_zero_iff | Submodule.mem_orthogonal_singleton_iff_inner_right |
| mathlib.module | Mathlib.Analysis.InnerProductSpace.Basic | Mathlib.Analysis.InnerProductSpace.Orthogonal |
| note | `inner_eq_zero_iff`/`Submodule.orthogonal` characterize orthogonality of vectors via vanishing inner product. | `Submodule.mem_orthogonal_singleton_iff_inner_right` characterizes orthogonality of vectors via vanishing inner product. |
modifiedFailure of cancellation law10210add0410
| Field | From #1171 | To #1974 |
|---|
| note | `exists_ne_zero_dotProduct_eq_zero` shows nonzero vectors with zero dot product exist, witnessing the failure of cancellation. | `Matrix.exists_ne_zero_dotProduct_eq_zero` shows nonzero vectors with zero dot product exist, witnessing the failure of cancellation. |
modifiedScalar triple product5e3f292b80eb
| Field | From #1171 | To #1974 |
|---|
| note | `triple_product_eq_det` states `u ⬝ᵥ v ⨯₃ w = det ![u, v, w]`, defining and identifying the scalar triple product. | `triple_product_eq_det` states `u ⬝ᵥ v ×₃ w = det ![u, v, w]`, identifying the scalar triple product with a determinant. |
modifiedVector triple product (Lagrange's formula)f5964847063c
| Field | From #1171 | To #1974 |
|---|
| note | `cross_cross` gives the Lie-bracket form of the vector triple product, but the BAC-CAB identity `u × (v × w) = (u·w) v − (u·v) w` is not stated explicitly. | `cross_cross` gives the Jacobi/Lie-bracket form of the triple cross product, but the BAC-CAB identity `u × (v × w) = (u·w) v − (u·v) w` is not stated explicitly. |
modifiedComplex dot productb5e2049d93e8
| Field | From #1171 | To #1974 |
|---|
| note | The complex Hermitian dot product is the inner product on `EuclideanSpace ℂ ι`, identified with `y ⬝ᵥ star x`. | The complex Hermitian dot product is the inner product on `EuclideanSpace ℂ ι`, identified by `EuclideanSpace.inner_eq_star_dotProduct` with `y ⬝ᵥ star x`. |
modifiedNorm squared of complex vectorc4bc419d0417
| Field | From #1171 | To #1974 |
|---|
| note | `norm_sq_eq_re_inner` is part of the `InnerProductSpace` definition: `‖x‖^2 = re ⟪x, x⟫`. | `InnerProductSpace.norm_sq_eq_re_inner` is part of the `InnerProductSpace` definition: `‖x‖^2 = re ⟪x, x⟫`. |
modifiedWeighted inner product2bbb0df48ae8
| Field | From #1171 | To #1974 |
|---|
| mathlib.decl | Matrix.PosSemidef.toInnerProductSpace | Matrix.toInnerProductSpace |
| note | Function-space weighted inner products can be obtained via `MeasureTheory.L2` with `μ.withDensity w`; the finite-dimensional weighted form is `Matrix.toInnerProductSpace`, but no dedicated weighted-function-space decl exists. | Function-space weighted inner products can be built from `MeasureTheory.L2` with `μ.withDensity w`; the finite-dimensional weighted form is `Matrix.toInnerProductSpace`, but no dedicated weighted-function-space decl exists. |
modifiedFrobenius inner productbdccc4c5097a
| Field | From #1171 | To #1974 |
|---|
| note | The Frobenius norm/inner product structure exists via `Matrix.frobeniusSeminormedAddCommGroup` (PiLp 2 on entries), but Mathlib lacks a directly named `frobeniusInner` declaration. | The Frobenius norm/inner-product structure exists via `Matrix.frobeniusSeminormedAddCommGroup` (PiLp 2 on entries), but Mathlib lacks a directly named `frobeniusInner` declaration. |