.

Author: PrParadoxy

QCLib/LinearAlgebra/StdBasis.lean

@@ -64,10 +64,16 @@ theorem Matrix.UnitaryGroup.ext_col [DecidableEq ι]
 
 variable [DecidableEq ι]
 
-theorem Matrix.UnitaryGroup.ext_smul_basis [Nonempty ι]
+open Matrix in
+@[simp]
+theorem Matrix.unitaryGroup.smul_euclidean_vec_def
+  {α m : Type*} [Fintype m] [DecidableEq m] [CommRing α] [StarRing α]
+    (U : unitaryGroup m α) (v : EuclideanSpace α m) : U • v = WithLp.toLp 2 (↑U *ᵥ v.ofLp) :=
+  PiLp.ext (congrFun rfl)
+
+theorem Matrix.UnitaryGroup.ext_smul_basis
     {U V : Matrix.unitaryGroup ι ℂ} : (∀ i : ι, (U • δ[i]) = V • δ[i]) → U = V := by
-  simp [basisVector_def, basisFun_apply, Submonoid.smul_def, ]
-  sorry
+  simpa [basisVector_def ] using ext_col
 
 @[simp]
 theorem Matrix.UnitaryGroup.diagonal_smul_basisVector