Zulip Chat Archive

Stream: Is there code for X?

Topic: int.coe_to_nat_eq


view this post on Zulip Eloi (Jul 19 2020 at 11:17):

I didn't find this in the library... Is there some similar lemma?

example (n:): 0  n  (n.to_nat) = n :=
  begin
    sorry,
  end

view this post on Zulip Rob Lewis (Jul 19 2020 at 11:19):

docs#int.to_nat_of_nonneg

view this post on Zulip Rob Lewis (Jul 19 2020 at 11:20):

library_search finds this (if you have data.int.basic imported)

view this post on Zulip Eloi (Jul 19 2020 at 11:29):

Thaks, I was searching manually in lib/lean/library/init/data.int.basic and I thought it was mathlib.


Last updated: May 19 2021 at 03:22 UTC