Zulip Chat Archive

Stream: maths

Topic: rational numbers

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

Kenny Lau (Jun 27 2020 at 19:08):

div_inj

Johan Commelin (Jun 27 2020 at 19:09):

I like that

Floris van Doorn (Jun 27 2020 at 22:36):

or perhaps div_int_inj

Last updated: Dec 20 2023 at 11:08 UTC