refactor(peps): move SameState symmetry to defs

Author: Sirui Lu

TNLean/PEPS/Defs.lean

@@ -65,6 +65,10 @@ noncomputable def stateCoeff (A : Tensor G d) (σ : V → Fin d) : ℂ :=
 def SameState (A B : Tensor G d) : Prop :=
   ∀ σ : V → Fin d, stateCoeff A σ = stateCoeff B σ
 
+/-- `SameState` is symmetric: it is equality of all state coefficients. -/
+theorem SameState.symm {A B : Tensor G d} (hAB : SameState A B) : SameState B A :=
+  fun σ => (hAB σ).symm
+
 /-- Vertex-wise injectivity: at each vertex `v`, the family of physical vectors
 `η ↦ A.component v η` (indexed by virtual configurations on the incident edges)
 is linearly independent in `Fin d → ℂ`.

TNLean/PEPS/InsertionAlgebra.lean

@@ -683,10 +683,6 @@ theorem edgeInsertedCoeff_injective (B : Tensor G d) (e : Edge G)
     simpa using this
   rw [hMN, hM'eqN]
 
-/-- `SameState` is symmetric: it is equality of all state coefficients. -/
-theorem SameState.symm {A B : Tensor G d} (hAB : SameState A B) : SameState B A :=
-  fun σ => (hAB σ).symm
-
 /-- The transfer map packaged as a `ℂ`-linear map, using additivity and
 homogeneity of `edgeTransferMatrix`. -/
 noncomputable def edgeTransferLinearMap (A B : Tensor G d) (e : Edge G)