smul_def

Mathlib.Algebra.Field.Defs

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

English

For any a ∈ ℚ and x ∈ K, the action a • x equals the product (a : K) · x.

Русский

Для любого a ∈ ℚ и x ∈ K скалярное действие a • x равно произведению (a : K) · x.

LaTeX

$$$a \in \mathbb{Q}, x \in K: a \cdot x = (a : K) x$$$

Lean4

theorem smul_def (a : ℚ) (x : K) : a • x = ↑a * x :=
  DivisionRing.qsmul_def a x

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

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

Разделы

Аффилиация

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