no goals
α : Type u_1
β : Type u_2
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
g f : CauSeq β abv
hf : f ≈ 0
this : LimZero (f - 0)
⊢ LimZero f
simpa
no goals
α : Type u_1
β : Type u_2
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
g f : CauSeq β abv
hf : f ≈ 0
this✝ : LimZero (f - 0)
this : LimZero (f * g)
⊢ LimZero (f * g - 0)
simpa