@[instance 300]
Equations
- Zero.toOfNat0 = { ofNat := Zero.zero }
@[instance 200]
Equations
- Zero.ofOfNat0 = { zero := 0 }
@[instance 300]
Equations
- One.toOfNat1 = { ofNat := One.one }
@[instance 200]
Equations
- One.ofOfNat1 = { one := 1 }
The fundamental scalar multiplication in an additive monoid.
nsmulRec n a = a+a+...+a
n times.
This function should not be used directly;
it is often used to implement an instance for scalar multiplication.