mathlib documentation

core.init.data.setoid

@[instance]
def setoid_has_equiv {α : Sort u} [setoid α] :

Equations
theorem setoid.refl {α : Sort u} [setoid α] (a : α) :
a a

theorem setoid.symm {α : Sort u} [setoid α] {a b : α} :
a bb a

theorem setoid.trans {α : Sort u} [setoid α] {a b c : α} :
a bb ca c