Generators fixed

Author: PrParadoxy

QCLib/Circuit/Hadamard.lean

@@ -59,7 +59,7 @@ private theorem HH_aux (y : Fin 2) :
 -- TBD: `simp` runs into a loop. Investigate.
 theorem HH_apply (k : Register n) : (HH n) • δ[k] = HadamardBasisVector n k := by
   simp_rw [HH_def, HadamardBasisVector, basisVector_eq_prod,
-    UnitaryGroup.piKroneckerUnitary_smul_vec, H_apply,
+    Matrix.UnitaryGroup.piKroneckerUnitary_smul_vec, H_apply,
     piOuterProduct_smul_const, HH_aux, piOuterProduct_univ_sum, Fintype.card_fin,
     piOuterProduct_smul_univ, Finset.prod_pow_eq_pow_sum]
 

QCLib/Circuit/PauliGroup/Generators.lean

@@ -38,7 +38,7 @@ Choose a namespace.
 
 public section
 
-open Complex Matrix Qubit
+open Complex Matrix Qubit EuclideanSpace
 
 open scoped PiOuterProduct
 

QCLib/LinearAlgebra/StdBasis.lean

@@ -56,9 +56,12 @@ open scoped ENNReal
 
 variable (p : ℝ≥0∞) (K K' : Type*) {K'' : Type*} (V : Type*) {V' V'' : Type*}
 
-@[to_additive (attr := simps)]
+@[to_additive]
 instance instOne [One V] : One (WithLp p V) := (WithLp.equiv p V).one
 
+lemma zero_def (p : ENNReal) (V : Type u_4) [Zero V] : 0 = (WithLp.equiv p V).symm 0 := rfl
+lemma one_def (p : ENNReal) (V : Type u_4) [One V] : 1 = (WithLp.equiv p V).symm 1 := rfl
+
 end WithLpMissingInstances.WithLp
 
 open EuclideanSpace PiOuterProduct Function
@@ -96,14 +99,16 @@ example [CommMonoid α] (f : (i : ι) → EuclideanSpace α (l i)) (j) :
 @[simp]
 theorem piOuterProduct_one [CommMonoid α] : (⨂ i, (1 : EuclideanSpace α (l i))) = 1 := by
   ext1
-  simp
+  simp only [WithLp.one_def, WithLp.equiv_symm_apply, ofLp_injective, Pi.piOuterProduct_one]
 
 @[simp]
 theorem piOuterProduct_zero [CommMonoidWithZero α] (f : Π i, EuclideanSpace α (l i))
     (h : ∃ i, f i = 0) : (⨂ i, f i) = 0 := by
   ext j
   obtain ⟨i, hi⟩ := h
-  simpa using Finset.prod_eq_zero (Finset.mem_univ i) (by simp [hi])
+  simpa [WithLp.zero_def] using
+    Finset.prod_eq_zero (Finset.mem_univ i)
+      (by simp [hi, WithLp.zero_def])
 
 @[simp]
 theorem piOuterProduct_smul [CommSemiring α] [DecidableEq ι]