dotProduct_pUnit — Mathlib

English

If both v and w are functions from the one-point type PUnit to α, then their dot product reduces to the product of the two values at the unique point.

Русский

Если обе функции заданы на единственной точке, то их скалярное произведение равно произведению их значений в этой точке.

LaTeX

$$$$\operatorname{dotProduct}(v,w) = v(\ast) \cdot w(\ast) \quad (v,w: PUnit \to \alpha).$$$$

Lean4

@[simp]
theorem dotProduct_pUnit [AddCommMonoid α] [Mul α] (v w : PUnit → α) : v ⬝ᵥ w = v ⟨⟩ * w ⟨⟩ := by simp [dotProduct]

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