added statement of translation invariant

Antoine-dSG · Jul 29, 2024 · ff63c11 · ff63c11
1 parent 28e547c
commit ff63c11
Showing 1 changed file with 6 additions and 0 deletions.
diff --git 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