Zulip Chat Archive

Stream: new members

Topic: lemmas related to core


view this post on Zulip Yakov Pechersky (Aug 13 2020 at 14:33):

Where would something like the lemma below go? The mod_eq_of_lt is in core.

@[simp] lemma one_mod_eq_one (n : ) : 1 % (n + 2) = 1 := by { exact nat.mod_eq_of_lt (add_lt_add_right n.succ_pos 1) }

view this post on Zulip Alex J. Best (Aug 13 2020 at 14:38):

data.nat.basic seems reasonable. (zero_mod for int is in data.int.basic for example)

view this post on Zulip Chris Wong (Aug 14 2020 at 08:45):

I think you can drop the exact and use term mode directly

view this post on Zulip Chris Wong (Aug 14 2020 at 08:45):

@[simp] lemma one_mod_eq_one (n : ) : 1 % (n + 2) = 1 :=
nat.mod_eq_of_lt (add_lt_add_right n.succ_pos 1)

view this post on Zulip Yakov Pechersky (Aug 14 2020 at 11:22):

#3763


Last updated: May 11 2021 at 13:22 UTC