Zulip Chat Archive
Stream: new members
Topic: 1 mod r
Michael Wahlberg (Apr 21 2023 at 01:46):
How do we prove this theorem
example(n : \N ) (hn : n > 3) : 1 % n = 1 : = by sorry
Moritz Doll (Apr 21 2023 at 02:16):
You want to use docs#nat.one_mod
Moritz Doll (Apr 21 2023 at 02:18):
together with something like docs#nat.sub_add_cancel
Last updated: May 02 2025 at 03:31 UTC