feat: add Fin.ofNat'_zero

2026-03-17 18:34:06 +00:00 · 2025-01-28 11:47:33 +11:00
1 changed files with 2 additions and 0 deletions
--- a/src/Init/Data/Fin/Lemmas.lean
+++ b/src/Init/Data/Fin/Lemmas.lean
@@ -13,6 +13,8 @@ import Init.Omega

 namespace Fin

+@[simp] theorem ofNat'_zero (n : Nat) [NeZero n] : Fin.ofNat' n 0 = 0 := rfl
+
@[deprecated Fin.pos (since := "2024-11-11")]
 theorem size_pos (i : Fin n) : 0 < n := i.pos