mathlib3
59cfa02f - chore(data/quot): rename `lift_on_beta` to `lift_on_mk` (#5921)

Commit
5 years ago
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](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/quotient.20.22on_beta.22.20vs.20.22on_mk.22) was unanimously in favor of this rename.
Author
Parents
Loading