mk_smul

Mathlib.Algebra.Order.Nonneg.Module

URI: https://scilib.ai/kg/mathlib#Nonneg.mk_smul

English

For any a ∈ R and ha ≥ 0, and x ∈ S, the action of the pair (a, ha) equals the action of a: (⟨a, ha⟩) • x = a • x.

Русский

Для любого a ∈ R и ha ≥ 0, и x ∈ S, действие пары (a, ha) равно действию a: (⟨a, ha⟩) • x = a • x.

LaTeX

$$$ (\\langle a, h a \\rangle) \\cdot x = a \\cdot x $$$

Lean4

@[simp]
theorem mk_smul (a) (ha) (x : S) : (⟨a, ha⟩ : R≥0) • x = a • x :=
  rfl

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

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

Разделы

Аффилиация

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