compProd_of_not_isSFiniteKernel_left

English

If the kernel κ is not S-finite, then κ ⊗ₖ η equals the zero kernel for any η.

Русский

Если ядро κ не является S- конечным, то произведение κ ⊗ₖ η равно нулю независимо от η.

LaTeX

$$$$\kappa \otimes_k \eta = 0,$$$$

Lean4

@[simp]
theorem compProd_of_not_isSFiniteKernel_left (κ : Kernel α β) (η : Kernel (α × β) γ) (h : ¬IsSFiniteKernel κ) :
    κ ⊗ₖ η = 0 := by simp [compProd, h]

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