Theorems · Theorem · commutative algebra

IsLinearTopology.tendsto_mul_zero_of_right

∀ {R : Type u_1} [inst : Ring R] [inst_1 : TopologicalSpace R] [IsLinearTopology R R] {ι : Type u_2} {f : Filter ι}
  (a b : ι → R), Filter.Tendsto b f (nhds 0) → Filter.Tendsto (a * b) f (nhds 0)

Defined in

Mathlib.Topology.Algebra.LinearTopology

Cited by

2 results in Mathlib

Foundations

Depth 22 from the axioms · uses propext, Quot.sound

Assumes

RingTopologicalSpaceIsLinearTopology