Mathlib v3 is deprecated. Go to Mathlib v4

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.

Estimated changes