coe_pointwise_smul

Mathlib.Algebra.Algebra.Subalgebra.Pointwise

URI: https://scilib.ai/kg/mathlib#Subalgebra.coe_pointwise_smul

English

The coercion of m • S equals m acting on the set S; i.e., the underlying set is preserved under scalar action.

Русский

Приведение к множесту показывает, что m • S работает на множесте S без изменения.

LaTeX

$$↑(m • S) = m • (S : Set A)$$

Lean4

@[simp, norm_cast]
theorem coe_pointwise_smul (m : R') (S : Subalgebra R A) : ↑(m • S) = m • (S : Set A) :=
  rfl

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

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

Разделы

Аффилиация

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