Description: The right module R induces a left module L by replacing the scalar multiplication with a reversed multiplication if the scalar ring is commutative. The hypothesis "rmodislmod.r" is a definition of a right module analogous to Definition df-lmod of a left module, see also islmod . (Contributed by AV, 3-Dec-2021) (Proof shortened by AV, 18-Oct-2024)
Ref | Expression | ||
---|---|---|---|
Hypotheses | rmodislmod.v | |
|
rmodislmod.a | |
||
rmodislmod.s | |
||
rmodislmod.f | |
||
rmodislmod.k | |
||
rmodislmod.p | |
||
rmodislmod.t | |
||
rmodislmod.u | |
||
rmodislmod.r | |
||
rmodislmod.m | |
||
rmodislmod.l | |
||
Assertion | rmodislmod | |