Quadratic AdjoinRoot reduction

The defining equation for the root of X² - d in its AdjoinRoot model.

@[simp]

theorem TauCeti.AdjoinRoot.root_sq {R : Type u_1} [CommRing R] (d : R) : AdjoinRoot.root (Polynomial.X ^ 2 - Polynomial.C d) ^ 2 = (algebraMap R (AdjoinRoot (Polynomial.X ^ 2 - Polynomial.C d))) d

The root of X² - d in its AdjoinRoot model squares to the coefficient d.