domCoprod'_apply — Mathlib

English

The simple-tensor evaluation of domCoprod' equals the corresponding domCoprod evaluation.

Русский

Простейшее тензорное применение domCoprod' совпадает с соответствующим domCoprod.

LaTeX

$$$domCoprod'_apply (a,b) = domCoprod (a,b).$$$

Lean4

@[simp]
theorem domCoprod'_apply (a : MultilinearMap R (fun _ : ι₁ => N) N₁) (b : MultilinearMap R (fun _ : ι₂ => N) N₂) :
    domCoprod' (a ⊗ₜ[R] b) = domCoprod a b :=
  rfl

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