Mathlib v3 is deprecated. Go to Mathlib v4

Theorem quotient.lift_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_betaView on Github →
2020-06-02 00:43
src/data/quot.lean
chore(*): split long lines (#2913)
Modified quotient.lift_betaView on Github →
2019-07-03 00:58
src/data/quot.lean
feat(measure_theory): Define Bochner integration (#1149) …
Modified quotient.lift_betaView on Github →
2018-03-08 11:25
data/quot.lean
feat(ring_theory): move localization
Added quotient.lift_betaView on Github →