dotProduct_comm — Mathlib

English

For α with an additive commutative monoid structure and a commuting multiplication, the dot product is symmetric: dotProduct(v,w) = dotProduct(w,v).

Русский

Пусть α имеет структуру коммутативного полууольшенного кольца; тогда скалярное произведение симметрично: dotProduct(v,w) = dotProduct(w,v).

LaTeX

$$$$\operatorname{dotProduct}(v,w) = \operatorname{dotProduct}(w,v).$$$$

Lean4

theorem dotProduct_comm [AddCommMonoid α] [CommMagma α] (v w : m → α) : v ⬝ᵥ w = w ⬝ᵥ v := by
  simp_rw [dotProduct, mul_comm]

Похожие утверждения