def definition def or abbrev

`tensor_product`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

  36def tensor_product {p₁ q₁ p₂ q₂ : ℕ}
  37  (_T₁ : Tensor p₁ q₁) (_T₂ : Tensor p₂ q₂) : Tensor (p₁ + p₂) (q₁ + q₂) := fun _ _ _ => 0

Definition body.

  38
  39/-- Canonical zero tensor. -/

Lean names referenced from this declaration's body.