## Stream: Is there code for X?

### Topic: iff.intro quotient.exact' quotient.sound'

#### Eric Wieser (Jan 19 2021 at 12:33):

Does this have a name? If not, what would be a good name for it?

#### Johan Commelin (Jan 19 2021 at 12:34):

I have no idea what the types of quotient.exact' and quotient.sound' are... so I don't know what this question is :wink:

#### Eric Wieser (Jan 19 2021 at 12:35):

I will update with the statement shortly...

#### Eric Wieser (Jan 19 2021 at 12:36):

lemma quotient.name_me {α : Type*} (x y : α) [s : setoid α] :
quotient.mk x = quotient.mk y ↔ x ≈ y :=
⟨quotient.exact, quotient.sound⟩

lemma quotient.name_me' {α : Type*} (x y : α) (s : setoid α) :
(quotient.mk' x : quotient s) = quotient.mk' y ↔ setoid.r x y :=
⟨quotient.exact', quotient.sound'⟩


#### Eric Wieser (Jan 19 2021 at 12:38):

Ah, it's docs#quotient.eq'

#### Kevin Buzzard (Jan 19 2021 at 12:53):

Your question reminds me that somewhere deep down in my job list is "write basic document on quotients explaining all the language used in mathlib"

#### Kevin Buzzard (Jan 19 2021 at 12:53):

For mathematicians it's particularly confusing, because we traditionally use lift to mean something else.

#### Eric Wieser (Jan 19 2021 at 12:58):

It probably doesn't help that the definitions and therefore documentation is split between core and mathlib

Last updated: May 16 2021 at 05:21 UTC