x y : ℝ*
hx : ¬Infinitesimal x
hy : Infinite y
⊢ Infinite (y * x)
x y : ℝ*
hx : ¬Infinitesimal x
hy : Infinite y
⊢ Infinite (x * y)
rw [mul_comm]
no goals
x y : ℝ*
hx : ¬Infinitesimal x
hy : Infinite y
⊢ Infinite (y * x)
exact infinite_mul_of_infinite_not_infinitesimal hy hx