mul

Mathlib.Topology.Algebra.UniformRing

URI: https://scilib.ai/kg/mathlib#UniformSpace.Completion.mul

English

The completed space is equipped with a multiplicative structure extending that on α.

Русский

Дополнение имеет умножение, расширяющее умножение в α.

LaTeX

$$$\\mathrm{Mul}(\\mathrm{Completion}(\\alpha))$$$

Lean4

instance mul : Mul (Completion α) :=
  ⟨curry <| (isDenseInducing_coe.prodMap isDenseInducing_coe).extend ((↑) ∘ uncurry (· * ·))⟩

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru