case h.e'_3
α : Type u
β : Type v
γ : Type w
a : ℝ
ha : a ≠ 0
⊢ ↑(↑(zmultiplesHom ℝ) a) = (fun x => x * a) ∘ Int.cast
α : Type u
β : Type v
γ : Type w
a : ℝ
ha : a ≠ 0
⊢ Tendsto (↑(↑(zmultiplesHom ℝ) a)) cofinite (cocompact ℝ)
convert (tendsto_cocompact_mul_right₀ ha).comp Int.tendsto_coe_cofinite
case h.e'_3.h
α : Type u
β : Type v
γ : Type w
a : ℝ
ha : a ≠ 0
n : ℤ
⊢ ↑(↑(zmultiplesHom ℝ) a) n = ((fun x => x * a) ∘ Int.cast) n
case h.e'_3
α : Type u
β : Type v
γ : Type w
a : ℝ
ha : a ≠ 0
⊢ ↑(↑(zmultiplesHom ℝ) a) = (fun x => x * a) ∘ Int.cast
ext n
no goals
case h.e'_3.h
α : Type u
β : Type v
γ : Type w
a : ℝ
ha : a ≠ 0
n : ℤ
⊢ ↑(↑(zmultiplesHom ℝ) a) n = ((fun x => x * a) ∘ Int.cast) n
simp