a b c q r : ℚ
hr : r.num = 0
hr' : r = 0
⊢ q / r = q.num * ↑r.den /. (↑q.den * r.num)
a b c q r : ℚ
hr : r.num = 0
⊢ q / r = q.num * ↑r.den /. (↑q.den * r.num)
have hr' : r = 0 := zero_of_num_zero hr
no goals
a b c q r : ℚ
hr : r.num = 0
hr' : r = 0
⊢ q / r = q.num * ↑r.den /. (↑q.den * r.num)
simp [*]
no goals
a b c q r : ℚ
hr : ¬r.num = 0
⊢ q * r⁻¹ = q.num /. ↑q.den * (r.num /. ↑r.den)⁻¹
simp [num_den]
no goals
a b c q r : ℚ
hr : ¬r.num = 0
⊢ q.num /. ↑q.den * (r.num /. ↑r.den)⁻¹ = q.num /. ↑q.den * (↑r.den /. r.num)
rw [inv_def']
no goals
a b c q r : ℚ
hr : ¬r.num = 0
⊢ ↑q.den ≠ 0
simpa using den_nz q