continuousSMul

Mathlib.Topology.Algebra.MulAction

URI: https://scilib.ai/kg/mathlib#Units.continuousSMul

English

The group of units Mˣ acts continuously on X.

Русский

Группа единиц Mˣ действует непрерывно на X.

LaTeX

$$ContinuousSMul Mˣ X$$

Lean4

@[to_additive]
instance continuousSMul : ContinuousSMul Mˣ X :=
  IsInducing.id.continuousSMul Units.continuous_val rfl

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

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

Разделы

Аффилиация

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