instMulActionSubtypeMem — Mathlib

English

The action by a subfield is the same as the ambient action, i.e., the subfield acts on X via the inclusion F → K.

Русский

Действие подполя на X совпадает с действием всего поля: F действует на X через включение F → K.

LaTeX

$$$ [MulAction K X] \\Rightarrow [MulAction F X] \\text{ with action } a\\cdot x := a\\cdot_K x$$

Lean4

/-- The action by a subfield is the action by the underlying field. -/
instance [MulAction K X] (F : Subfield K) : MulAction F X :=
  inferInstanceAs (MulAction F.toSubsemiring X)

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