cancel division in polynomials

Stream: Is there code for X?

[Eric Rodriguez]

I currently have this result:

lemma cyclotomic_dvd_geom_sum_of_dvd {d n : ℕ} (hdn : d ∣ n) (hd : d ≠ 1) :
  cyclotomic d ℤ ∣ geom_sum X n :=

I'd like to be able to derive (hd : d ∣ n) (hd0 : d ≠ 0) (hdn : d < n) : (cyclotomic n ℤ).eval q ∣ (q ^ n - 1) / (q ^ d - 1) (or well, the polynomial version) from this easily. However, I don't see any way to do this; div_by_monic doesn't seem to have any cancellation theorems at all! Is it just worth it to prove the appropriate result for geom_sum directly, instead?

[Riccardo Brasca]

I would avoid using /ₘ at all, and just providing the quotient explicitly.

[Riccardo Brasca]

By "explicitly" I mean using some other divisibility result, not the actual formula.

[Riccardo Brasca]

We know that q ^ d - 1 divides q ^ n - 1?

[Eric Rodriguez]

amazingly, it seems not

[Riccardo Brasca]

It's docs#commute.geom_sum₂_mul , isn't it? Take n = d, x = q ^(n/d) and y = 1 or something like that.

[Riccardo Brasca]

Why docs# doesn't work?! This theorem

[Kevin Buzzard]

because of the \_2 I believe