Prod instances for NoZeroSMulDivisors

This file defines a NoZeroSMulDivisors instance for the binary product of actions.

instance Prod.noZeroSMulDivisors {R : Type u_1} {M : Type u_2} {N : Type u_3} [Zero R] [Zero M] [Zero N] [SMulWithZero R M] [SMulWithZero R N] [NoZeroSMulDivisors R M] [NoZeroSMulDivisors R N] : NoZeroSMulDivisors R (M × N)

Equations

• ⋯ = ⋯