lemma proved wrapper

`intCast_ne_zero_of_ne_zero`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

 243private lemma intCast_ne_zero_of_ne_zero {z : ℤ} (hz : z ≠ 0) : ((z : ℤ) : ℝ) ≠ 0 := by

One-line wrapper that applies exact_mod_cast.

 244  exact_mod_cast hz
 245