Zulip Chat Archive

Stream: general

Topic: proof for quotient.mk

ZHAO Jinxiang (Jun 11 2022 at 16:40):

example {α: Type*}  (s: setoid α) (a b: α) : @quotient.mk _ s a = @quotient.mk _ s b  setoid.r a b :=

Can we proof it step by step? I don't know what happen in it.

Eric Wieser (Jun 11 2022 at 16:44):

docs#quotient.eq is a proof of exactly that statement (with different notation on the right)

Eric Wieser (Jun 11 2022 at 16:45):

When using quotient.mk, you're supposed to talk about x ≈ y not setoid.r x y

Eric Wieser (Jun 11 2022 at 16:46):

When using quotient.mk', setoid.r is the preferred spelling (see docs#quotient.eq')

ZHAO Jinxiang (Jun 11 2022 at 16:57):

I can't find the definition of quot.mk in std lib. Is this function built into the language?

Markus Himmel (Jun 11 2022 at 17:02):

Yes, see core.lean

Last updated: Aug 03 2023 at 10:10 UTC