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

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