pairingDual_tprod_tprod — Mathlib

English

Evaluating pairingDual on pure tensors in both arguments yields the product of individual evaluations f_i(v_i).

Русский

Оценивание pairingDual на чистых тензорах в обеих координатах даёт произведение значений f_i(v_i).

LaTeX

$$$ pairingDual\\; R\\; M\\; n (tprod\\; R\\; f) (tprod\\; R\\; v) = \\prod_i f_i(v_i) $$$

Lean4

@[simp]
theorem pairingDual_tprod_tprod (f : (_ : Fin n) → Module.Dual R M) (v : Fin n → M) :
    pairingDual R M n (tprod _ f) (tprod _ v) = ∏ i, (f i (v i)) := by simp [pairingDual]

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