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

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