Description: Scalar product of a finite group sum for a left module over a semiring. (Contributed by Thierry Arnoux, 16-Mar-2018)
Ref | Expression | ||
---|---|---|---|
Hypotheses | gsumvsca.b | |
|
gsumvsca.g | |
||
gsumvsca.z | |
||
gsumvsca.t | |
||
gsumvsca.p | |
||
gsumvsca.k | |
||
gsumvsca.a | |
||
gsumvsca.w | |
||
gsumvsca1.n | |
||
gsumvsca1.c | |
||
Assertion | gsumvsca1 | |