Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-04-20 15:36 8adfafd9

View on Github →

feat(data/nat,data/int): add some modular arithmetic lemmas (#2460) These lemmas (a) were found useful in formalising solutions to some olympiad problems, see https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/Some.20olympiad.20formalisations; (b) seem more generally relevant than to just those particular problems; (c) do not show up through library_search as being already present.

Estimated changes