one_dotProduct_one — Mathlib

English

The total unit dot product over the whole index set equals the cardinality of the index set: dotProduct(1,1) = card(n).

Русский

Сумма единичного скалярного произведения по всем индексам равна кардинальности множества индексов: dotProduct(1,1) = card(n).

LaTeX

$$$$ \operatorname{dotProduct}(1,1) = \lvert n \rvert. $$$$

Lean4

@[simp]
theorem one_dotProduct_one : (1 : n → α) ⬝ᵥ 1 = Fintype.card n := by simp [dotProduct]

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