  30  fun x up low => (1/2 : ℝ) * (T x up low - T x up (fun i => if (i : ℕ) = 0 then low 1 else low 0))
  31
  32/-- Index contraction collapses to the zero tensor. -/
  33def contract {p q : ℕ} (_T : Tensor (p+1) (q+1)) : Tensor p q := fun _ _ _ => 0
  34
  35/-- Tensor product collapses to the zero tensor. -/
  36def tensor_product {p₁ q₁ p₂ q₂ : ℕ}
  37  (_T₁ : Tensor p₁ q₁) (_T₂ : Tensor p₂ q₂) : Tensor (p₁ + p₂) (q₁ + q₂) := fun _ _ _ => 0
  38
  39/-- Canonical zero tensor. -/
  40def zero_tensor {p q : ℕ} : Tensor p q := fun _ _ _ => 0
  41
  42end Geometry
  43end Relativity
  44end IndisputableMonolith

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.