Mathlib v3 is deprecated. Go to Mathlib v4

Theorem quotient.lift_on_beta₂

Modification history

2021-02-05 00:51
src/data/quot.lean
chore(data/quot): rename `lift_on_beta` to `lift_on_mk` (#5921) …
Deleted quotient.lift_on_beta₂View on Github →
2020-10-08 05:32
src/data/quot.lean
chore(data/quot): `quot.mk` etc are surjective (#4517)
Modified quotient.lift_on_beta₂View on Github →
2020-07-20 03:39
src/data/quot.lean
feat(data/quot.lean): add lift_on_beta\_2 (#3456) …
Added quotient.lift_on_beta₂View on Github →