Documentation

Schlessinger.Mathlib.Algebra.Module.Commutative

source
def Commutative.RightModule.instModuleMulOpposite_schlessinger (R : Type u_1) (M : Type u_2) [CommSemiring R] [AddCommMonoid M] [Module R M] :
Module Rᵐᵒᵖ M
Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem Commutative.RightModule.instIsCentralScalar_schlessinger (R : Type u_1) (M : Type u_2) [CommSemiring R] [AddCommMonoid M] [Module R M] :
    IsCentralScalar R M
    source
    @[simp]
    theorem Commutative.RightModule.op_smul (R : Type u_1) (M : Type u_2) [CommSemiring R] [AddCommMonoid M] [Module R M] (r : R) (x : M) :
    MulOpposite.op r • x = r • x