instSMulWithZeroSubtypeMem — Mathlib

English

The intermediate field induces a Module structure on X via the ambient field.

Русский

Промежуточное поле задаёт структуру модуля на X через окружающее поле.

LaTeX

$$$\\text{Module } F X$ is inherited from $\\text{Module } L X$$$

Lean4

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

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