Typeclass One

Zero has already been defined in Lean.

class One (α : Type u) : Type u

• one : α

Instances

• AddMonoid.End.instOne
• AddOpposite.instOne
• Associates.instOne
• LO.FirstOrder.ModelOfSatEq.instOneOfOne
• LO.FirstOrder.Structure.Model.instOneOfOne
• Monoid.End.instOne
• MulOpposite.instOne
• Nonneg.one
• One.ofOfNat1
• Part.instOne
• Pi.instOne
• Positive.instOneSubtypeLtOfNat
• Prod.instOne
• RingHom.instOne
• Units.instOne
• WithBot.one
• WithOne.one
• WithTop.one
• WithZero.one
• instOneLex
• instOneMonoidHom
• instOneMulHom
• instOneMultiplicativeOfZero
• instOneOneHom
• instOneOrderDual
• instOnePNat

@[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 }

@[instance 20]

instance Zero.instNonempty {α : Type u} [Zero α] : Nonempty α

@[instance 20]

instance One.instNonempty {α : Type u} [One α] : Nonempty α

theorem Subsingleton.eq_one {α : Type u} [One α] [Subsingleton α] (a : α) : a = 1

theorem Subsingleton.eq_zero {α : Type u} [Zero α] [Subsingleton α] (a : α) : a = 0