smulDivisionRing

Mathlib.Algebra.Field.Defs

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

English

There is a canonical ℚ-action on K given by qsmul, i.e., a ℚ-vector-space structure on K.

Русский

Существует каноническое действие ℚ на K, задающее структуру векторного пространства над ℚ.

LaTeX

$$$\text{SMul}_{\mathbb{Q}} K \\text{exists with the action given by } qsmul$$$

Lean4

instance (priority := 100) smulDivisionRing : SMul ℚ K :=
  ⟨DivisionRing.qsmul⟩

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

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

Разделы

Аффилиация

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