Documentation

Mathlib.Init.ZeroOne

Classes for Zero and One #

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