Factorizations

Stream: FLT-regular

[Alex J. Best]

After quite a lot longer than I expected I have a proof of a version of the identity
$x^p + y^p = \prod_i (x + \zeta_i y),$
this is now pow_add_pow_eq_prod_add_zeta_mul in number_theory.cyclotomic.factoring.

This is the first line of the proof of https://leanprover-community.github.io/flt-regular/sect0004.html#theorem:FLT_case_one in the blueprint.

The reason it took so much effort to prove a fairly simple identity is I decided to go for a proof that would be maximally useful in the future instead of just proving this identity directly, and proved this via homogenization of the corresponding univariate identity $x^p + 1 = \prod_i x + \zeta_i$. So that hopefully if anyone else needs such homogenous identity / factorization in future it will be easier to prove with this api. Also it seems like mathlib would want to be able to homogenize polynomials eventually anyway.
This ended up adding about a 1000 lines on homogenization, leading terms of multivariate polynomials and assorted other junk. All of this is definitely relevant and hopefully useful in mathlib, so I'll try and PR it bit by bit in the near future. Some nice side results are things like the fact that the total degree of a multivariate polynomial adds when multiplying polynomials over a domain.

I'm not 100% sure exactly which version of this factorization is the most helpful, but hopefully other versions (e.g. integral ones) will be easy to construct from here.

[Alex J. Best]

After quite a lot longer than I expected I have a proof of a version of the identity
$x^p + y^p = \prod_i (x + \zeta_i y),$
this is now pow_add_pow_eq_prod_add_zeta_mul in number_theory.cyclotomic.factoring.

This is the first line of the proof of https://leanprover-community.github.io/flt-regular/sect0004.html#theorem:FLT_case_one in the blueprint.

The reason it took so much effort to prove a fairly simple identity is I decided to go for a proof that would be maximally useful in the future instead of just proving this identity directly, and proved this via homogenization of the corresponding univariate identity $x^p + 1 = \prod_i x + \zeta_i$. So that hopefully if anyone else needs such homogenous identity / factorization in future it will be easier to prove with this api. Also it seems like mathlib would want to be able to homogenize polynomials eventually anyway.
This ended up adding about a 1000 lines on homogenization, leading terms of multivariate polynomials and assorted other junk. All of this is definitely relevant and hopefully useful in mathlib, so I'll try and PR it bit by bit in the near future. Some nice side results are things like the fact that the total degree of a multivariate polynomial adds when multiplying polynomials over a domain.

I'm not 100% sure exactly which version of this factorization is the most helpful, but hopefully other versions (e.g. integral ones) will be easy to construct from here.