Zulip Chat Archive
Stream: maths
Topic: Naming request
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
Yury G. Kudryashov (Jun 30 2020 at 21:14):
Do we have this for fields?
Yury G. Kudryashov (Jun 30 2020 at 21:15):
Probably not but if I'm wrong, then please use the same name
Patrick Stevens (Jul 01 2020 at 06:27):
I couldn't find any prior art, sadly
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: Dec 20 2023 at 11:08 UTC