smul_closure

Mathlib.Algebra.GroupWithZero.Submonoid.Pointwise

URI: https://scilib.ai/kg/mathlib#AddSubmonoid.smul_closure

English

The smul functor commutes with closure: m • closure S = closure (m • S).

Русский

Умножение коммутирует со сверткой: m • closure S = closure (m • S).

LaTeX

$$$ m \cdot \mathrm{closure}(S) = \mathrm{closure}(m \cdot S) $$$

Lean4

@[simp]
theorem smul_closure (m : M) (s : Set A) : m • closure s = closure (m • s) :=
  AddMonoidHom.map_mclosure _ _

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

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

Разделы

Аффилиация

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