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.