q : ℚ
x y : ℝ
h : Irrational x
m : ℤ
hm : m ≠ 0
⊢ Irrational (x * ↑↑m)
q : ℚ
x y : ℝ
h : Irrational x
m : ℤ
hm : m ≠ 0
⊢ Irrational (x * ↑m)
rw [← cast_coe_int]
q : ℚ
x y : ℝ
h : Irrational x
m : ℤ
hm : m ≠ 0
⊢ ↑m ≠ 0
q : ℚ
x y : ℝ
h : Irrational x
m : ℤ
hm : m ≠ 0
⊢ Irrational (x * ↑↑m)
refine' h.mul_rat _
no goals
q : ℚ
x y : ℝ
h : Irrational x
m : ℤ
hm : m ≠ 0
⊢ ↑m ≠ 0
rwa [Int.cast_ne_zero]