From e5c073aa4940937a081227f67fb0b5a27d741113 Mon Sep 17 00:00:00 2001 From: Antoine-dSG Date: Wed, 24 Jul 2024 14:08:04 +0800 Subject: [PATCH] fixed typo --- FriezePatterns/chapter1.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/FriezePatterns/chapter1.lean b/FriezePatterns/chapter1.lean index c10d691..331aec7 100644 --- a/FriezePatterns/chapter1.lean +++ b/FriezePatterns/chapter1.lean @@ -81,5 +81,5 @@ def set_1_to_n (n : Nat) : Set Nat := { i | 1 ≤ i ∧ i ≤ n } -- The class below looks a bit dubious to me -class closedFrieze (f : ℕ × ℕ → ℚ) (n : ℕ) extends closedPattern f where - positive_n : ∀m, ∀ i ∈ (set_1_to_n n), f (i,m) > 0 +--class closedFrieze (f : ℕ × ℕ → ℚ) (n : ℕ) extends closedPattern f where + -- positive_n : ∀m, ∀ i ∈ (set_1_to_n n), f (i,m) > 0