# Documentation

Mathlib.Init.Data.Quot

# Quotient types #

These are ported from the Lean 3 standard library file init/data/quot.lean.

inductive EqvGen {α : Type u} (r : ααProp) :
ααProp

EqvGen r is the equivalence relation generated by r.

Instances For
theorem EqvGen.is_equivalence {α : Type u} (r : ααProp) :
def EqvGen.Setoid {α : Type u} (r : ααProp) :

EqvGen.Setoid r is the setoid generated by a relation r.

The motivation for this definition is that Quot r behaves like Quotient (EqvGen.Setoid r), see for example Quot.exact and Quot.EqvGen_sound.

Equations
• = { r := , iseqv := (_ : ) }
theorem Quot.exact {α : Type u} (r : ααProp) {a : α} {b : α} (H : Quot.mk r a = Quot.mk r b) :
EqvGen r a b
theorem Quot.EqvGen_sound {α : Type u} {r : ααProp} {a : α} {b : α} (H : EqvGen r a b) :
Quot.mk r a = Quot.mk r b
instance Quotient.decidableEq {α : Sort u} {s : } [d : (a b : α) → Decidable (a b)] :
Equations
• One or more equations did not get rendered due to their size.