instMulDistribMulActionSubtypeMem

English

If X carries a faithful K-action, then the restricted F-action on X is also faithful.

Русский

Если X имеет верное действие K на X, то ограниченное до F действие на X также верно.

LaTeX

$$$ [SMul K X] [FaithfulSMul K X] (F : Subfield K) : FaithfulSMul F X$$

Lean4

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

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