[Merged by Bors] - chore(ring_theory/polynomial/cyclotomic): use ratfunc

[ericrbg]

---

welcome to the most work anyone has ever done to remove a nontrivial on an unused lemma,,,

[ericrbg]

the build seems to be working but I still get an X :( ignore github, CI is fine with this

[Vierkantor]

LGTM. Using ratfunc R rather than a parameter K is slightly less general, however it does look nicer. So I'll let you decide whether to make this change.

[Vierkantor]

I had to generalize ratfunc K to also accept is_domain K, not just field K: #10428. But then it works for free by replacing K with ratfunc K:

Suggested change

	lemma cyclotomic_eq_prod_X_pow_sub_one_pow_moebius {n : ℕ} (R : Type*) [comm_ring R]
	{K : Type*} [field K] [algebra (polynomial R) K] [is_fraction_ring (polynomial R) K] :
	algebra_map _ K (cyclotomic n R) =
	∏ i in n.divisors_antidiagonal, (algebra_map (polynomial R) K (X ^ i.snd - 1)) ^ μ i.fst :=
	lemma cyclotomic_eq_prod_X_pow_sub_one_pow_moebius {n : ℕ} (R : Type*) [comm_ring R] [is_domain R] :
	algebra_map _ (ratfunc R) (cyclotomic n R) =
	∏ i in n.divisors_antidiagonal, (algebra_map (polynomial R) _ (X ^ i.snd - 1)) ^ μ i.fst :=

There are also some changed Ks below, but github doesn't allow me to make suggestions there...

[ericrbg]

I think we should just close this PR and open a separate one; also, @riccardobrasca what do you think of this change?

[riccardobrasca]

LGTM too. Can we evaluate a rational function? If we already have that, the (currently not so nice) proof of polynomial.cyclotomic_coeff_zero should be golfed.

[Vierkantor]

Yes, ratfunc.eval should work as expected (except when dividing by 0 of course!)

[ericrbg]

we can't golf the proof, sadly, as coeff_zero works for all comm_rings

[riccardobrasca]

I think we can prove it for Z and then use that cyclotomic n R comes from cyclotomic n Z.

[ericrbg]

I keep missing this and just saying "can't be done"! need to turn on my brain instead of just being in Lean mode all the time. Anyways, I currently have a sorry-free proof of ∀x, eval (cyclotomic n ℝ) x > 0 waiting for #10422, which is actually necessary for this proof (ratfunc.eval is only multiplicative if there isn't division by zero, and then we can split the product as required). There's also some issues with ratfunc ℤ.eval (namely that it doesn't work, and diamonds (seem to?) happen if you try generalize to [comm_ring K] [is_domain K]), but these can be easily dealt with by going to ℚ instead so there's no problems there.

[riccardobrasca]

Well, mathematically there is only cyclotomic n Z. In Lean it is convenient to have cyclotomic n R, but it comes from Z by definition. If something is wrong with integers coefficients we should fix it

[riccardobrasca]

So if the constant term of cyclotomic n Z is 1 the same is true for cyclotomic n R

[ericrbg]

yes I agree, I'm just laying out some of the issues that happen in Lean; there's nothing wrong with integer coeffs, just it's far more convenient to work over a field with ratfunc, and the suffices work out so that we do indeed get the result for all R.

[jcommelin]

Thanks 🎉

bors merge

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests