roll back changes that should have gone to other branch

Author: goliath-klein

QCLib/Circuit/Gate/Qubit.lean

@@ -9,7 +9,6 @@ public import Mathlib.LinearAlgebra.Matrix.Hermitian
 public import QCLib.LinearAlgebra.UnitaryGroup.RootsOfUnity
 public import QCLib.LinearAlgebra.StdBasis
 public import QCLib.Misc.OrderOf
-public import Mathlib.Analysis.InnerProductSpace.PiL2
 
 import QCLib.Misc.IntCast
 
@@ -78,7 +77,8 @@ noncomputable def T : 𝐔[Qubit] :=
 
 noncomputable def R (k : ℕ) : 𝐔[Qubit] := ⟨!![1, 0; 0, ζ (2^k)], by
   rw [Matrix.mem_unitaryGroup_iff]
-  matrix_expand ⟩
+  matrix_expand
+  ⟩
 
 @[matrixExpand]
 theorem H_eq : H.val = (√(1/2) : ℂ) • !![1, 1; 1, -1] := by rfl
@@ -291,8 +291,6 @@ def mns : (Qubit → ℂ) := ((√2)⁻¹ : ℂ) • (δ[0] - δ[1])
 def lft : (Qubit → ℂ) := ((√2)⁻¹ : ℂ) • (δ[0] + I • δ[1])
 def rgt : (Qubit → ℂ) := ((√2)⁻¹ : ℂ) • (δ[0] - I • δ[1])
 
-def upl2 : EuclideanSpace
-
 end
 
 example : pls = (√2)⁻¹ • ![1, 1] := by matrix_expand [pls]

QCLib/LinearAlgebra/StdBasis.lean

@@ -38,9 +38,6 @@ This file also collects `•` application
 noncomputable def BasisVector {ι : Type*} [Finite ι] (i : ι) : (ι → ℂ) :=
   Pi.basisFun ℂ ι i
 
-noncomputable def l2BasisVector {ι : Type*} [Finite ι] (i : ι) : (ι → ℂ) :=
-  Pi.basisFun ℂ ι i
-
 @[matrixExpand]
 theorem basisVector_def (ι : Type*) [Finite ι] (i : ι) :
   BasisVector i = Pi.basisFun ℂ ι i := by rfl