no goals
F : Type ?u.19834
ι : Type ?u.19837
α : Type u_1
β : Type ?u.19843
inst✝ : DivisionRing α
n : ℤ
d : ℕ
h : d ≠ 0
c : Nat.coprime (Int.natAbs n) d
⊢ ↑(-mk' n d) = -↑(mk' n d)
simpa only [cast_def] using
  show (↑(-n) / d : α) = -(n / d) by
    rw [div_eq_mul_inv, div_eq_mul_inv, Int.cast_neg, neg_mul_eq_neg_mul]
no goals
F : Type ?u.19834
ι : Type ?u.19837
α : Type u_1
β : Type ?u.19843
inst✝ : DivisionRing α
n : ℤ
d : ℕ
h : d ≠ 0
c : Nat.coprime (Int.natAbs n) d
⊢ ↑(-n) / ↑d = -(↑n / ↑d)
rw [div_eq_mul_inv, div_eq_mul_inv, Int.cast_neg, neg_mul_eq_neg_mul]