theorem HexRealRootsTheory.Tarski.rootSum_mod {R : Type u_1} [Field R] [LinearOrder R] (p q : Polynomial R) (a b : Hex.Endpoint R) : rootSum p (q % p) a b = rootSum p q a b

Reducing a query modulo its head preserves its signed sum at head roots, including zero heads, repeated roots and infinite endpoints.