Zulip Chat Archive

Stream: maths

Topic: rational numbers


view this post on Zulip Paul van Wamelen (Jun 27 2020 at 19:07):

Does anyone have a good suggestion for the name for:

lemma name_me {a b c d : } (hb0 : 0 < b) (hd0 : 0 < d)
  (h1 : nat.coprime a.nat_abs b.nat_abs) (h2 : nat.coprime c.nat_abs d.nat_abs)
  (h : (a : ) / b = (c : ) / d) : a = c  b = d

view this post on Zulip Kenny Lau (Jun 27 2020 at 19:08):

div_inj

view this post on Zulip Johan Commelin (Jun 27 2020 at 19:09):

I like that

view this post on Zulip Floris van Doorn (Jun 27 2020 at 22:36):

or perhaps div_int_inj


Last updated: May 09 2021 at 11:09 UTC