instMulActionSubtypeMem — Mathlib

English

There is a canonical MulAction of S on α inherited from the ambient algebra action.

Русский

Существует каноничeское действие MulAction S на α, унаследованное от действия над окружавшей алгеброй.

LaTeX

$$$\text{MulAction } S \alpha$ (inherited from A)$$

Lean4

/-- The action by a subalgebra is the action by the underlying algebra. -/
instance [MulAction A α] (S : Subalgebra R A) : MulAction S α :=
  inferInstanceAs (MulAction S.toSubsemiring α)

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