domCoprodDep'_apply — Mathlib

English

The value of domCoprodDep' on a simple tensor a ⊗ b is exactly domCoprodDep a b.

Русский

Значение domCoprodDep' на элементе-tensor a ⊗ b равно domCoprodDep a b.

LaTeX

$$$domCoprodDep' (a \otimes b) = domCoprodDep(a,b).$$$

Lean4

@[simp]
theorem domCoprodDep'_apply (a : MultilinearMap R (fun i₁ ↦ N (.inl i₁)) N₁)
    (b : MultilinearMap R (fun i₂ ↦ N (.inr i₂)) N₂) : domCoprodDep' (a ⊗ₜ b) = domCoprodDep a b := by rfl

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