instSMulSubtypeMem — Mathlib

English

The scalar multiplication by an element of an intermediate field on a module equals the scalar multiplication by its image in the ambient field.

Русский

Умножение скаляра элемента промежуточного поля на модуль равно умножению этого элемента на его образ в верхнем поле.

LaTeX

$$$g \\cdot m = (g : L) \\cdot m$$$

Lean4

/-- The action by an intermediate field is the action by the underlying field. -/
instance [SMul L X] (F : IntermediateField K L) : SMul F X :=
  inferInstanceAs (SMul F.toSubfield X)

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