Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-06-25 06:32 3875012a

View on Github →

feat(data/quot): add map', hrec_on', and hrec_on₂' (#3148) Also add a few simp lemmas

Estimated changes

Modified src/data/quot.lean

modified theorem quotient.choice_eq

added theorem quotient.hrec_on'_mk'

added theorem quotient.hrec_on₂'_mk'

added theorem quotient.map'_mk'

added theorem quotient.map_mk

added theorem quotient.map₂'_mk'