instMulSemiringActionSubtypeMem — Mathlib

English

If a monoid M acts on a semiring R with MulSemiringAction, then for any Submonoid S ≤ M, the subtype corresponding to S inherits a MulSemiringAction on R by restriction.

Русский

Если моноид M действует на полукольцо R с помощью MulSemiringAction, то для любого подмонойда S ⊆ M подмножество S наследует MulSemiringAction на R через ограничение.

LaTeX

$$$S \\le M \\implies MulSemiringAction (Subtype\\ (fun x => x \\in S)) R$$

Lean4

instance (priority := low) [MulSemiringAction M R] {S : Type*} [SetLike S M] (s : S) [SubmonoidClass S M] :
    MulSemiringAction s R :=
  { inferInstanceAs (DistribMulAction s R), inferInstanceAs (MulDistribMulAction s R) with }

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