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 : α} (hab : a b) :
b a

theorem setoid.trans {α : Sort u} [setoid α] {a b c : α} (hab : a b) (hbc : b c) :
a c