Documentation

Mathlib.Init.ZeroOne

Classes for Zero and One #

class Zero (α : Type u) :
  • zero : α
Instances
    @[instance 300]
    instance Zero.toOfNat0 {α : Type u_1} [Zero α] :
    OfNat α 0
    Equations
    • Zero.toOfNat0 = { ofNat := Zero.zero }
    @[instance 200]
    instance Zero.ofOfNat0 {α : Type u_1} [OfNat α 0] :
    Zero α
    Equations
    • Zero.ofOfNat0 = { zero := 0 }
    class One (α : Type u) :
    • one : α
    Instances
      @[instance 300]
      instance One.toOfNat1 {α : Type u_1} [One α] :
      OfNat α 1
      Equations
      • One.toOfNat1 = { ofNat := One.one }
      @[instance 200]
      instance One.ofOfNat1 {α : Type u_1} [OfNat α 1] :
      One α
      Equations
      • One.ofOfNat1 = { one := 1 }
      @[match_pattern, deprecated]
      def bit0 {α : Type u} [Add α] (a : α) :
      α
      Equations
      Instances For
        @[match_pattern, deprecated]
        def bit1 {α : Type u} [One α] [Add α] (a : α) :
        α
        Equations
        Instances For