Revision #1974 → #2384 · back to history
modifiedDot product (algebraic, coordinates)dc295b54b347
| Field | From #1974 | To #2384 |
|---|
| mathlib.decl | Matrix.dotProduct | dotProduct |
| note | `Matrix.dotProduct v w := ∑ i, v i * w i` is exactly the algebraic coordinate definition. | `dotProduct v w := ∑ i, v i * w i` (root namespace, not `Matrix.dotProduct`) is exactly the algebraic coordinate definition. |
modifiedHomogeneity and distributivityc8c94f0ada2f
| Field | From #1974 | To #2384 |
|---|
| mathlib.decl | Matrix.add_dotProduct | add_dotProduct |
| note | `Matrix.add_dotProduct`, `dotProduct_add`, `smul_dotProduct`, `dotProduct_smul` (and corresponding inner-product lemmas) give bilinearity. | `add_dotProduct`, `dotProduct_add`, `smul_dotProduct`, `dotProduct_smul` (root namespace) give bilinearity of `⬝ᵥ`. |
modifiedCommutativity of the real dot product44c1ed45fbb3
| Field | From #1974 | To #2384 |
|---|
| mathlib.decl | Matrix.dotProduct_comm | dotProduct_comm |
| note | `Matrix.dotProduct_comm` proves `v ⬝ᵥ w = w ⬝ᵥ v` over commutative magmas; the inner-product version is `real_inner_comm`. | `dotProduct_comm` (root namespace) proves `v ⬝ᵥ w = w ⬝ᵥ v` over commutative magmas; the inner-product version is `real_inner_comm`. |
modifiedAssociativity with scalar multiplication6175746c1f03
| Field | From #1974 | To #2384 |
|---|
| mathlib.decl | Matrix.smul_dotProduct | smul_dotProduct |
| note | `Matrix.smul_dotProduct` and `Matrix.dotProduct_smul` give `(c • v) ⬝ᵥ w = c • (v ⬝ᵥ w)`. | `smul_dotProduct` and `dotProduct_smul` (root namespace) give `(c • v) ⬝ᵥ w = c • (v ⬝ᵥ w)`. |
modifiedFailure of cancellation law10210add0410
| Field | From #1974 | To #2384 |
|---|
| mathlib.decl | Matrix.exists_ne_zero_dotProduct_eq_zero | exists_ne_zero_dotProduct_eq_zero |
| note | `Matrix.exists_ne_zero_dotProduct_eq_zero` shows nonzero vectors with zero dot product exist, witnessing the failure of cancellation. | `exists_ne_zero_dotProduct_eq_zero` (root namespace) shows nonzero vectors with zero dot product exist, witnessing the failure of cancellation. |
addedCatastrophic cancellation in floating-point dot productcad7c9719e3c