A classical theorem in rational homotopy theory says that a space is formal over $\mathbb{Q}$ iff it is formal over any field of characteristic zero. In other words, the algebra $A^*_{PL}(X)$ is formal iff $A^*_{PL}(X) \otimes_\mathbb{Q} \mathbb{K}$ is formal, for some extension of $\mathbb{Q}$. (Probably with some nilpotency conditions on $X$.) This is for Corollary 6.9 in the paper of Halperin–Stasheff below.
A theorem of Guillén Santos–Navarro–Pascual–Roig (Theorem 6.2.1 from the paper below) says that if $P$ is is an operad in chains over some field $\Bbbk$ of characteristic zero, and if $\mathbb{K}$ is an extension of $\Bbbk$, then $P$ is formal iff $P \otimes_\Bbbk \mathbb{K}$ is formal. In particular, if $P$ is a topological operad, then $C_*(P;\mathbb{Q})$ is formal iff $C_*(P;\mathbb{R})$ is formal.
Probably a stupid question, but is it known whether the same is true for cooperads in commutative dg-algebras (AKA Hopf cooperads)? In particular, given a topological operad, does formality of $A^*_{PL}(P) \otimes_\mathbb{Q} \mathbb{R}$ imply formality of $A^*_{PL}(P)$?
Halperin, Stephen; Stasheff, James. "Obstructions to homotopy equivalences." in Adv. Math. 32, 233–279 (1979; Zbl 0408.55009)
Guillén Santos, F.; Navarro, F.; Pascual, P.; Roig, A. "Moduli spaces and formal operads" in Duke Math. J. 129, No. 2, 291–335 (2005)
