Mathlib v3 is deprecated. Go to Mathlib v4

Theorem surjective_quotient_mk

Modification history

2020-10-08 05:32

src/data/quot.lean

chore(data/quot): `quot.mk` etc are surjective (#4517)

Added surjective_quotient_mk View on Github →