a b c : ℚ
n d : ℤ
⊢ n /. 1 / (d /. 1) = n /. d
a b c : ℚ
n d : ℤ
⊢ ↑n / ↑d = n /. d
repeat' rw [coe_int_eq_divInt]
no goals
a b c : ℚ
n d : ℤ
⊢ n /. 1 / (d /. 1) = n /. d
exact divInt_div_divInt_cancel_left one_ne_zero n d
a b c : ℚ
n d : ℤ
⊢ n /. 1 / (d /. 1) = n /. d
a b c : ℚ
n d : ℤ
⊢ n /. 1 / (d /. 1) = n /. d
rw [coe_int_eq_divInt]