Commit 2022-12-22 21:16 c2c04cea

View on Github →

feat: port data.nat.even_odd_rec (#1148) First commit for data.nat.even_odd_rec Mathlib commit : ba2245edf0c8bb155f1569fd9b9492a9b384cde6

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/Nat/EvenOddRec.lean

added def Nat.evenOddRec

added theorem Nat.evenOddRec_even

added theorem Nat.evenOddRec_odd

added theorem Nat.evenOddRec_zero