From 582295a9edaa011fa2c5ef83732a7b2d1cbfca6a Mon Sep 17 00:00:00 2001 From: Kim Morrison <kim@tqft.net> Date: Wed, 4 Sep 2024 13:40:56 +1000 Subject: [PATCH] chore: missing lemma about Fin.ofNat' --- src/Init/Data/Fin/Lemmas.lean | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/src/Init/Data/Fin/Lemmas.lean b/src/Init/Data/Fin/Lemmas.lean index 2ee40b879b1d..253669475265 100644 --- a/src/Init/Data/Fin/Lemmas.lean +++ b/src/Init/Data/Fin/Lemmas.lean @@ -54,6 +54,11 @@ theorem mk_val (i : Fin n) : (⟨i, i.isLt⟩ : Fin n) = i := Fin.eta .. @[simp] theorem val_ofNat' (a : Nat) (is_pos : n > 0) : (Fin.ofNat' a is_pos).val = a % n := rfl +@[simp] theorem ofNat'_val_eq_self (x : Fin n) (h) : (Fin.ofNat' x h) = x := by + ext + rw [val_ofNat', Nat.mod_eq_of_lt] + exact x.2 + @[simp] theorem mod_val (a b : Fin n) : (a % b).val = a.val % b.val := rfl