instSMulPosStrictMono

Mathlib.Data.DFinsupp.Order

URI: https://scilib.ai/kg/mathlib#DFinsupp.instSMulPosStrictMono

← MathLib Explorer

English

The instance provides PosSMulStrictMono for the DFinsupp type when component-wise holds.

Русский

Инстанс задаёт PosSMulStrictMono для DFinsupp при выполнении компонентно.

LaTeX

$$$\text{PosSMulStrictMono}(\Pi_i \beta i)$ via DFinsupp$$

Lean4

instance instSMulPosStrictMono [∀ i, SMulPosStrictMono α (β i)] : SMulPosStrictMono α (Π₀ i, β i) :=
  SMulPosStrictMono.lift _ coe_le_coe coe_smul coe_zero

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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