Merge branch 'main' of github.com:AntoineChambert-Loir/DividedPowers4

AntoineChambert-Loir · Jun 5, 2024 · 5ebd019 · 5ebd019
2 parents 1fc3af2 + b986c62
commit 5ebd019
Showing 1 changed file with 2 additions and 2 deletions.
diff --git a/DividedPowers/ForMathlib/CombinatoricsLemmas.lean b/DividedPowers/ForMathlib/CombinatoricsLemmas.lean
@@ -5,8 +5,8 @@ import Mathlib.Data.Nat.Choose.Vandermonde
 section Combinatorics
 
 -- Because mathlib hasn't it yet!
-@[eliminator]
-theorem Nat.rec' {motive : Nat → Sort*}
+@[induction_eliminator]
+def Nat.rec' {motive : Nat → Sort*}
     (zero : motive 0) (add_one : (n : Nat) → motive n → motive (n + 1)) (t : Nat) :
     motive t :=
   Nat.rec zero add_one t