sumElim_dotProduct_sumElim

Mathlib.Data.Matrix.Mul

URI: https://scilib.ai/kg/mathlib#sumElim_dotProduct_sumElim

English

If α is AddCommMonoid and CommMagma, then dotProduct(v,w) = dotProduct(w,v).

Русский

При наличии AddCommMonoid и CommMagma скалярное произведение симметрично: dotProduct(v,w) = dotProduct(w,v).

LaTeX

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

Lean4

@[simp]
theorem sumElim_dotProduct_sumElim : Sum.elim u x ⬝ᵥ Sum.elim v y = u ⬝ᵥ v + x ⬝ᵥ y := by simp [dotProduct]

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru