Commit 2021-02-05 00:51 59cfa02f

View on Github →

chore(data/quot): rename lift_on_beta to lift_on_mk (#5921) This also renames some other lift_*_beta lemmas to match their statement. The Zulip thread was unanimously in favor of this rename.

Estimated changes

Modified src/algebra/ring_quot.lean

Modified src/data/dfinsupp.lean

Modified src/data/multiset/functor.lean

deleted theorem multiset.lift_beta

added theorem multiset.lift_coe

Modified src/data/quot.lean

added theorem quot.lift_mk

added theorem quot.lift_on_mk

modified theorem quot.lift_on₂_mk

modified theorem quot.lift₂_mk

deleted theorem quotient.lift_beta

added theorem quotient.lift_mk

deleted theorem quotient.lift_on_beta

deleted theorem quotient.lift_on_beta₂

added theorem quotient.lift_on_mk

added theorem quotient.lift_on₂_mk

Modified src/data/setoid/basic.lean

Modified src/group_theory/congruence.lean

Modified src/ring_theory/nullstellensatz.lean

Modified src/ring_theory/valuation/basic.lean