int.div_eq_zero

Stream: Is there code for X?

[Johan Commelin]

example (d n : ℤ) (h : d ∣ n) (H : n / d = 0) : n = 0 :=
begin
  sorry
end

[Johan Commelin]

Or is there some edge case if d = 0??

[Anne Baanen]

If d = 0 then n = 0 since d \| n.

[Anne Baanen]

example (d n : ℤ) (h : d ∣ n) (H : n / d = 0) : n = 0 :=
begin
  rw [← int.mul_div_cancel' h, H, mul_zero]
end

[Johan Commelin]

Merci!