Commit 2025-12-22 09:02 839af0cc

feat(RingTheory/MvPolynomial/IrrQuadratic): irreducibility of sum X_i Y_i (#31161) The quadratic polynomial $$\sum_i c_i X_i Y_i$$ is irreducible, provided the following three conditions holds:

• the ground ring is a domain
• there are at least 2 nonzero $$c_i$$
• only units of $$R$$ divide all $$c_i$$. This was used in the initial proof that the transvections have determinant 1. Now, a more general result is proved there and this PR is no more needed. I believe that it remains of independent interest (irreducibility of quadrics in algebraic geometry) but the maintainers might want that the general one.