Module properties of dual numbers #
The coordinatewise scalar action on dual numbers commutes with multiplication. These instances make bilinear multiplication and convolution available with that module structure. Dual numbers over an Artinian ring are also Artinian, using their product module structure.
instance
TauCeti.dualNumberIsScalarTower
{R : Type u_1}
{B : Type u_2}
[CommSemiring R]
[Semiring B]
[Algebra R B]
:
IsScalarTower R (DualNumber B) (DualNumber B)
Coordinatewise scalar multiplication associates with multiplication of dual numbers.
instance
TauCeti.dualNumberSMulCommClass
{R : Type u_1}
{B : Type u_2}
[CommSemiring R]
[Semiring B]
[Algebra R B]
:
SMulCommClass R (DualNumber B) (DualNumber B)
Coordinatewise scalar multiplication commutes with left multiplication of dual numbers.
Dual numbers over an Artinian ring form an Artinian ring.