Documentation

Init.Data.Zero

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

@[instance 300]
instance Zero.toOfNat0 {α : Type u_1} [Zero α] :
OfNat α 0
Equations
@[instance 200]
instance Zero.ofOfNat0 {α : Type u_1} [OfNat α 0] :
Zero α
Equations

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

@[instance 300]
instance One.toOfNat1 {α : Type u_1} [One α] :
OfNat α 1
Equations
@[instance 200]
instance One.ofOfNat1 {α : Type u_1} [OfNat α 1] :
One α
Equations
def npowRec {M : Type u_1} [One M] [Mul M] :
NatMM

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
Instances For
    def nsmulRec {M : Type u_1} [Zero M] [Add M] :
    NatMM

    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
    Instances For