smul_def

Mathlib.Algebra.Field.Defs

URI: https://scilib.ai/kg/mathlib#NNRat.smul_def

English

In a DivisionSemiring K, the scalar action of q ≥ 0 on a is given by q • a = (q : K) · a.

Русский

В делимом полe K скалярное действие q ≥ 0 на элемент a задаётся как q • a = (q : K) · a.

LaTeX

$$$(q : \mathbb{Q}_{\ge 0}) \cdot a = (q : K) \cdot a$$$

Lean4

theorem smul_def (q : ℚ≥0) (a : K) : q • a = q * a :=
  DivisionSemiring.nnqsmul_def q a

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

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

Разделы

Аффилиация

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