## 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: May 18 2021 at 08:14 UTC