Theorem: factorize3 (ECTate/Algebra/EllipticCurve/AuxRingLemmas.lean)

State before:
R : Type u
inst✝ : CommRing R
root p : R
q : ℕ
⊢ 3 * (root * p ^ q * (root * p ^ q)) = p ^ q * p ^ q * (3 * root * root)
Tactic:
ring
State after:
no goals