English
If R has the discrete topology and A is a topological semiring with an R-algebra structure, then R acts continuously on A; i.e., ContinuousSMul R A.
Русский
Если R имеет дискретную топологию и A является топологическим полукольцом с структурой R-алгебры, то действие R на A непрерывно; то есть ContinuousSMul R A.
LaTeX
$$$\\operatorname{ContinuousSMul}~R~A$$$
Lean4
/-- If `R` is a discrete topological ring, then any topological ring `S` which is an `R`-algebra
is also a topological `R`-algebra.
NB: This could be an instance but the signature makes it very expensive in search.
See https://github.com/leanprover-community/mathlib4/pull/15339
for the regressions caused by making this an instance. -/
theorem instContinuousSMul [IsTopologicalSemiring A] [DiscreteTopology R] : ContinuousSMul R A :=
continuousSMul_of_algebraMap _ _ continuous_of_discreteTopology
