From ff63c111df3afc67a3dba9cf88ecd42a8f0c190e Mon Sep 17 00:00:00 2001
From: Antoine-dSG <adsg96@hku.hk>
Date: Mon, 29 Jul 2024 20:19:35 +0800
Subject: [PATCH] added statement of translation invariant

---
 FriezePatterns/Chapter1/section1.lean | 6 ++++++
 1 file changed, 6 insertions(+)

diff --git a/FriezePatterns/Chapter1/section1.lean b/FriezePatterns/Chapter1/section1.lean
index d129d1d..eda3358 100644
--- a/FriezePatterns/Chapter1/section1.lean
+++ b/FriezePatterns/Chapter1/section1.lean
@@ -108,3 +108,9 @@ theorem glideSymm (F : Type*) [Field F] (f : ℕ×ℕ → F) (n: ℕ) [nzPattern
  have h : f (1,m+n+1) = f (n,m) := by exact firstRowSymm F f n m
  exact Eq.symm h
  sorry
+
+
+-- This is a consequence of the glide symmetry
+lemma translateInvar (F : Type*) [Field F] (f : ℕ×ℕ → F) (i n: ℕ) [nzPattern_n F f n] (hi : i ≤ n+1) : ∀ m, f (i,m) = f (i,m+n+3) := by
+  intro m
+  sorry