instDistribMulActionSubtypeMem — Mathlib

English

The intermediate field acts on X via the underlying field action, i.e., the MulAction is inherited.

Русский

Промежуточное поле действует на X через действие базового поля; MulAction наследуется.

LaTeX

$$$\\forall a\\in F, \\forall x\\in X: a \\cdot x = (a : L) \\cdot x$$$

Lean4

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

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