Nevanlinna/tensor.lean

@@ -1,47 +0,0 @@
-import Mathlib.Analysis.InnerProductSpace.PiL2
-
-
-open RCLike Real Filter
-open Topology ComplexConjugate
-open LinearMap (BilinForm)
-open TensorProduct
-open InnerProductSpace
-open Inner
-
-
-example
-  {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
-  {F : Type*} [NormedAddCommGroup F] [InnerProductSpace ℝ F]
-  : 1 = 0 := by
-
-  let e : E →ₗ[ℝ] E →ₗ[ℝ] ℝ := innerₗ E 
-  let f : F →ₗ[ℝ] F →ₗ[ℝ] ℝ := innerₗ F 
-  let e₂ :=  TensorProduct.map₂ e f
-  let l := TensorProduct.lid ℝ ℝ 
-
-  have : ∀ e1 e2 : E, ∀ f1 f2 : F, e₂ (e1 ⊗ f1) (e2 ⊗ f2) = 
-
-  let X : InnerProductSpace.Core ℝ (E ⊗[ℝ] F) := {
-    inner := by
-      intro a b
-      exact TensorProduct.lid ℝ ℝ ((TensorProduct.map₂ (innerₗ E) (innerₗ F)) a b)
-    conj_symm := by
-      simp
-      intro x y
-
-      unfold innerₗ
-      
-      simp
-      sorry
-    nonneg_re := _
-    definite := _
-    add_left := _
-    smul_left := _
-  }
-
-  let inner : E ⊗[𝕜] E → E ⊗[𝕜] E → 𝕜 := 
-    --let x := TensorProduct.lift
-    --E.inner
-    --TensorProduct.map₂
-    sorry
-  sorry