instSMulSubtypeMem_1

Mathlib.FieldTheory.IntermediateField.Basic

URI: https://scilib.ai/kg/mathlib#IntermediateField.instSMulSubtypeMem_1

English

The scalar multiplication on the subtype S is inherited from the ambient algebra, giving a well-defined action of S on the subtype of E.

Русский

Скалярное умножение на подтипе S наследуется от внешней алгебры и задаёт корректное действие S на подполье E.

LaTeX

$$$\\text{SMul } S\\,\\bigl(\\text{Subtype mem } S\\; E\\bigr)$$$

Lean4

instance : SMul S T :=
  Algebra.toSMul

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

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

Разделы

Аффилиация

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