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

State before:
R : Type u
inst✝ : CommRing R
a b c r p : R
⊢ p ^ 3 * a + p * r * (p ^ 2 * b) + (p * r) ^ 2 * (p ^ 1 * c) + (p * r) ^ 3 = p ^ 3 * (a + r * b + r ^ 2 * c + r ^ 3)
Tactic:
ring
State after:
no goals