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

@[implicit_reducible, instance 300]

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

Equations

• Zero.toOfNat0 = { ofNat := Zero.zero }

@[implicit_reducible, instance 200]

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

Equations

• Zero.ofOfNat0 = { zero := 0 }

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

@[implicit_reducible, instance 300]

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

Equations

• One.toOfNat1 = { ofNat := One.one }

@[implicit_reducible, instance 200]

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

Equations

• One.ofOfNat1 = { one := 1 }

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.

Equations

• npowRec 0 x✝ = 1
• npowRec n.succ x✝ = npowRec n x✝ * x✝

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.

Equations

• nsmulRec 0 x✝ = 0
• nsmulRec n.succ x✝ = nsmulRec n x✝ + x✝