pointwise_smul_def

Mathlib.Algebra.GroupWithZero.Subgroup

URI: https://scilib.ai/kg/mathlib#AddSubgroup.pointwise_smul_def

English

The pointwise smul is defined by a • S = S.map (DistribMulAction.toAddMonoidEnd M A a).

Русский

Точечное smul задаётся формулой a • S = S.map (DistribMulAction.toAddMonoidEnd M A a).

LaTeX

$$$ a \\cdot S = S.map(\\\\DistribMulAction.toAddMonoidEnd(M,A,a))$$$

Lean4

theorem pointwise_smul_def (S : AddSubgroup A) : a • S = S.map (DistribMulAction.toAddMonoidEnd _ _ a) :=
  rfl

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

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

Разделы

Аффилиация

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