Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-10-08 05:32 34a44717

View on Github →

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

Estimated changes

Modified src/data/quot.lean

modified theorem quotient.lift_on_beta₂

added theorem quotient.surjective_quotient_mk'

added theorem surjective_quot_mk

added theorem surjective_quotient_mk