pi_apply — Mathlib

English

For a family Q_i of quadratic maps, the value of pi Q at a point x is the sum over i of Q_i(x_i).

Русский

Для семейства квадратичных отображений Q_i модульной системы значение pi Q в точке x равно сумме по i от Q_i(x_i).

LaTeX

$$$ \\pi Q(x) = \\sum_i Q_i(x_i). $$$

Lean4

@[simp]
theorem pi_apply [Fintype ι] (Q : ∀ i, QuadraticMap R (Mᵢ i) P) (x : ∀ i, Mᵢ i) : pi Q x = ∑ i, Q i (x i) :=
  sum_apply _ _ _

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