Commit 2025-05-11 01:02 fb1ce6eb

View on Github →

chore(*): use notation for dotProduct (#24733)

Estimated changes

Modified Mathlib/Analysis/InnerProductSpace/PiL2.lean

Modified Mathlib/Combinatorics/Configuration.lean

modified theorem Configuration.ofField.crossProduct_eq_zero_of_dotProduct_eq_zero

Modified Mathlib/Combinatorics/SimpleGraph/AdjMatrix.lean

Modified Mathlib/Data/Matrix/Hadamard.lean

Modified Mathlib/Data/Matrix/Mul.lean

Modified Mathlib/Data/Matrix/Notation.lean

modified theorem Matrix.dotProduct_empty

Modified Mathlib/Data/Matrix/Reflection.lean

Modified Mathlib/LinearAlgebra/Matrix/BilinearForm.lean

Modified Mathlib/LinearAlgebra/Matrix/DotProduct.lean

modified theorem dotProduct_eq

modified theorem dotProduct_eq_iff

modified theorem dotProduct_eq_zero

modified theorem dotProduct_eq_zero_iff

modified theorem dotProduct_nonneg_of_nonneg

modified theorem dotProduct_self_star_eq_zero

modified theorem dotProduct_self_star_nonneg

modified theorem dotProduct_star_self_eq_zero

modified theorem dotProduct_star_self_nonneg

Modified Mathlib/LinearAlgebra/Matrix/Nondegenerate.lean

Modified Mathlib/LinearAlgebra/Matrix/Orthogonal.lean

Modified Mathlib/LinearAlgebra/Matrix/PosDef.lean

Modified Mathlib/LinearAlgebra/Matrix/Trace.lean

Modified Mathlib/LinearAlgebra/Projectivization/Constructions.lean

Modified Mathlib/Order/Basic.lean

Modified Mathlib/Topology/Instances/Matrix.lean

deleted theorem Continuous.matrix_dotProduct