English
Let a,b,c,d ∈ ℤ with hb0: 0 < b, hd0: 0 < d, h1: Nat.Coprime a.natAbs b.natAbs, h2: Nat.Coprime c.natAbs d.natAbs, and h: (a : ℚ) / b = (c : ℚ) / d. Then a = c and b = d.
Русский
Пусть a,b,c,d ∈ ℤ, 0 < b, 0 < d, Nat.Coprime(a.natAbs, b.natAbs), Nat.Coprime(c.natAbs, d.natAbs) и (a/ b) = (c/ d) в ℚ. Тогда a = c и b = d.
LaTeX
$$$\\forall a,b,c,d \\in \\mathbb{Z},\\ 0 < b \\land 0 < d \\land Nat.Coprime(a.natAbs,b.natAbs) \\land Nat.Coprime(c.natAbs,d.natAbs) \\land \\frac{a}{b} = \\frac{c}{d} \\Rightarrow a=c \\land b=d$$$
Lean4
theorem div_int_inj {a b c d : ℤ} (hb0 : 0 < b) (hd0 : 0 < d) (h1 : Nat.Coprime a.natAbs b.natAbs)
(h2 : Nat.Coprime c.natAbs d.natAbs) (h : (a : ℚ) / b = (c : ℚ) / d) : a = c ∧ b = d :=
by
apply And.intro
· rw [← num_div_eq_of_coprime hb0 h1, h, num_div_eq_of_coprime hd0 h2]
· rw [← den_div_eq_of_coprime hb0 h1, h, den_div_eq_of_coprime hd0 h2]
