instMulActionSubtypeMem — Mathlib

English

The action by an intermediate field on a module coincides with the action by the ambient field.

Русский

Действие промежуточного поля на модуле совпадает с действием над окружающим полем.

LaTeX

$$$\\forall g\\in F,\\ \\forall m\\in X:\\ g \\cdot m = (g : L) \\cdot m$$$

Lean4

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

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