instMulSemiringActionSubtypeMem — Mathlib

English

The intermediate field induces a MulAction on X when X has a Monoid structure compatible with L.

Русский

Промежуточное поле индуцирует MulAction на X, если X имеет монойную структуру, совместимую с L.

LaTeX

$$$\\text{MulAction } F X$ inherited from $\\text{MulAction } L X$$$

Lean4

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

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