Commit 2022-12-13 10:52 91af1f8a

View on Github →

feat port: Data.Nat.Set (#961) cf9386b56953fb40904843af98b7a80757bbe7f9 Easy

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/Nat/Set.lean

added theorem Nat.range_casesOn

added theorem Nat.range_of_succ

added theorem Nat.range_rec

added theorem Nat.zero_union_range_succ