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.