Zulip Chat Archive

Stream: maths

Topic: Naming request


view this post on Zulip Patrick Stevens (Jun 30 2020 at 19:08):

What should the following be called? It's hard to express associativity in names.

lemma div_div_div {a b c : } (dvd : c  a) (dvd2 : a  b) : (b / (a / c)) / c = b / a := by sorry

view this post on Zulip Yury G. Kudryashov (Jun 30 2020 at 21:14):

Do we have this for fields?

view this post on Zulip Yury G. Kudryashov (Jun 30 2020 at 21:15):

Probably not but if I'm wrong, then please use the same name

view this post on Zulip Patrick Stevens (Jul 01 2020 at 06:27):

I couldn't find any prior art, sadly

view this post on Zulip Yury G. Kudryashov (Jul 01 2020 at 18:48):

BTW, you don't need a | b for this lemma. You can rw [nat.div_div_eq_div_mul, nat.div_mul_cancel]


Last updated: May 18 2021 at 08:14 UTC