Instances converting between Zero α and OfNat α (nat_lit 0).

@[instance 300]

instance Zero.toOfNat0 {α : Type u_1} [Zero α] : OfNat α 0

@[instance 200]

instance Zero.ofOfNat0 {α : Type u_1} [OfNat α 0] : Zero α

Instances converting between One α and OfNat α (nat_lit 1).

@[instance 300]

instance One.toOfNat1 {α : Type u_1} [One α] : OfNat α 1

@[instance 200]

instance One.ofOfNat1 {α : Type u_1} [OfNat α 1] : One α

def npowRec {M : Type u_1} [One M] [Mul M] : Nat → M → M

The fundamental power operation in a monoid. npowRec n a = a*a*...*a n times. This function should not be used directly; it is often used to implement a Pow M Nat instance, but end users should use the a ^ n notation instead.

def nsmulRec {M : Type u_1} [Zero M] [Add M] : Nat → M → M

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.