Prod instances for additive and multiplicative actions #
This file defines instances for binary product of additive and multiplicative actions and provides
scalar multiplication as a homomorphism from
α × β to
Main declarations #
See also #
Porting notes #
This was not done as part of the port in order to stay as close as possible to the mathlib3 code.