smul_inl

Mathlib.Algebra.Group.Action.Sum

URI: https://scilib.ai/kg/mathlib#Sum.smul_inl

English

The left injection Coe preserves the action: a · inl b = inl (a · b).

Русский

Левая вложенная часть сохраняет действие: a • inl b = inl (a • b).

LaTeX

$$$a \cdot (\mathrm{inl} \, b) = \mathrm{inl}(a \cdot b).$$$

Lean4

@[to_additive (attr := simp)]
theorem smul_inl : a • (inl b : α ⊕ β) = inl (a • b) :=
  rfl

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

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

Разделы

Аффилиация

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