smul_le_smul_left

Mathlib.Algebra.Ring.Submonoid.Pointwise

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

English

For a submonoid T ⊆ R and a family of submonoids {S_i} ⊆ A, T • (sup_i S_i) = sup_i (T • S_i).

Русский

Для подпмоноида T ⊆ R и семейства подмоноидов {S_i} ⊆ A выполняется T • (sup_i S_i) = sup_i (T • S_i).

LaTeX

$$$T \cdot \left( \bigsqcup_i S_i \right) = \bigsqcup_i (T \cdot S_i)$$$

Lean4

theorem smul_le_smul_left (h : M ≤ M') : M • P ≤ M' • P :=
  smul_le_smul h le_rfl

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

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

Разделы

Аффилиация

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