distribMulAction' — Mathlib

English

If S is a monoid acting on R and M compatibly, then there is a DistribMulAction on M/P given by a • [x] = [a • x].

Русский

Если S образует полное моноидальное действие на R и M совместимо, то на M/P существует DistribMulAction: a • [x] = [a • x].

LaTeX

$$$\forall a \in S,\forall [x] \in M/P,\ a \cdot [x] = [a \cdot x]$$$

Lean4

instance distribMulAction' [Monoid S] [SMul S R] [DistribMulAction S M] [IsScalarTower S R M] (P : Submodule R M) :
    DistribMulAction S (M ⧸ P) :=
  fast_instance%Function.Surjective.distribMulAction { toFun := mk, map_zero' := rfl, map_add' := fun _ _ => rfl }
      Quot.mk_surjective (Submodule.Quotient.mk_smul P)

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