Square roots in the complexification of a real closed field

QuadraticAlgebra.isSquare specializes the algebraic square-root construction to a real closed field, without requiring an order on that field as a hypothesis. This square-closure property is used to prove algebraic closedness of the complexification.

The semireal square obstruction supplies the field instance on QuadraticAlgebra R (-1) 0.

theorem QuadraticAlgebra.isSquare {R : Type u_1} [Field R] [IsRealClosed R] (z : QuadraticAlgebra R (-1) 0) : IsSquare z

Every element of R[i] is a square when R is real closed, without choosing an order.