Squares and finite products #
If all but the last entries of two finite families agree modulo squares, agreement of their products modulo squares determines the last entry. This is useful when prescribing the last coefficient of a diagonal quadratic form from its determinant.
theorem
TauCeti.isSquare_div_last_of_isSquare_div_prod
{G : Type u_1}
[CommGroup G]
{n : ℕ}
{a b : Fin (n + 1) → G}
(h : ∀ (i : Fin n), IsSquare (a i.castSucc / b i.castSucc))
(hp : IsSquare ((∏ i : Fin (n + 1), a i) / ∏ i : Fin (n + 1), b i))
:
Agreement modulo squares of two products, and of all their factors except the last, forces agreement of the last factors.