continuous_mul_of_finite — Mathlib

English

If D is a finite R-algebra with module topology, then multiplication on D is continuous; hence D becomes a topological ring.

Русский

Если D является конечно-регулярной R-алгеброй и на D задана модульная топология, умножение на D непрерывно, следовательно, D образует топологическое кольцо.

LaTeX

$$$\\text{Continuous\_mul}(D) \\;\\land\\; \\text{ModuleFinite}(R,D) \\Rightarrow \\text{Continuous}(\\,\\cdot\\,) : D\\times D \\to D$$$

Lean4

/-- If `D` is an `R`-algebra, finite as an `R`-module, and if `D` has the module topology,
then multiplication on `D` is automatically continuous. -/
@[continuity, fun_prop]
theorem continuous_mul_of_finite : Continuous (fun ab ↦ ab.1 * ab.2 : D × D → D) :=
  -- Proof: multiplication is bilinear so this follows from previous results.

  continuous_bilinear_of_finite_left (LinearMap.mul R D)

Похожие утверждения