## 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

I like that

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

or perhaps div_int_inj

Last updated: May 09 2021 at 11:09 UTC