Commit 2020-07-20 03:39 501aeb7f
View on Github →feat(data/quot.lean): add lift_on_beta_2 (#3456)
This corresponds to lift_on\_2
in library/init/data/quot.lean
just as lift_beta
and lift_on_beta
correspond to lift
and lift_on
. It greatly simplifies quotient proofs but was, surprisingly, missing.