ring_nf
case mk.mk
c : ℤα
z✝¹ w✝¹ z✝ w✝ : ℤ
⊢ ↑z✝¹ * ↑z✝ - 2 * ↑w✝¹ * ↑w✝ + (↑z✝¹ * ↑w✝ + ↑w✝¹ * ↑z✝ + ↑w✝¹ * ↑w✝) * complexα =
    (↑z✝¹ + ↑w✝¹ * complexα) * (↑z✝ + ↑w✝ * complexα)
case mk.mk
c : ℤα
z✝¹ w✝¹ z✝ w✝ : ℤ
⊢ ↑z✝¹ * ↑z✝ + ↑z✝¹ * ↑w✝ * complexα + (↑z✝ * ↑w✝¹ * complexα - ↑w✝¹ * ↑w✝ * 2) + ↑w✝¹ * ↑w✝ * complexα =
    ↑z✝¹ * ↑z✝ + ↑z✝¹ * ↑w✝ * complexα + ↑z✝ * ↑w✝¹ * complexα + ↑w✝¹ * ↑w✝ * complexα ^ 2