Theorems · Definition · commutative algebra

Submodule.pointwiseDistribMulAction

{α : Type u_1} →
  {R : Type u_2} →
    {M : Type u_3} →
      [inst : Semiring R] →
        [inst_1 : AddCommMonoid M] →
          [inst_2 : Module R M] →
            [inst_3 : Monoid α] →
              [inst_4 : DistribMulAction α M] → [SMulCommClass α R M] → DistribMulAction α (Submodule R M)

The action on a submodule corresponding to applying the action to every element. This is available as an instance in the Pointwise locale.

Defined in

Mathlib.Algebra.Module.Submodule.Pointwise

Cited by

105 results in Mathlib

Foundations

Depth 67 from the axioms, rests on 955 definitions · uses propext, Classical.choice, Quot.sound

Assumes

SemiringAddCommMonoidModuleMonoidDistribMulActionSMulCommClass