Theorem: ℤθ.simp_norm (Mordell4/CubicRing.lean)

State before:
a✝ b✝ c : ℤθ
a b : ℤ
⊢ norm { f := a, g := -b, h := 0 } = |a ^ 3 + 3 * a ^ 2 * b + 6 * a * b ^ 2 + 2 * b ^ 3|
Tactic:
unfold norm
State after:
a✝ b✝ c : ℤθ
a b : ℤ
⊢ |{ f := a, g := -b, h := 0 }.f ^ 3 - 2 * { f := a, g := -b, h := 0 }.g ^ 3 + 4 * { f := a, g := -b, h := 0 }.h ^ 3 -
                    3 * { f := a, g := -b, h := 0 }.f ^ 2 * { f := a, g := -b, h := 0 }.g -
                  3 * { f := a, g := -b, h := 0 }.f ^ 2 * { f := a, g := -b, h := 0 }.h +
                6 * { f := a, g := -b, h := 0 }.f * { f := a, g := -b, h := 0 }.g ^ 2 +
              6 * { f := a, g := -b, h := 0 }.g ^ 2 * { f := a, g := -b, h := 0 }.h +
            24 * { f := a, g := -b, h := 0 }.f * { f := a, g := -b, h := 0 }.h ^ 2 -
          12 * { f := a, g := -b, h := 0 }.g * { f := a, g := -b, h := 0 }.h ^ 2 -
        12 * { f := a, g := -b, h := 0 }.f * { f := a, g := -b, h := 0 }.g * { f := a, g := -b, h := 0 }.h| =
    |a ^ 3 + 3 * a ^ 2 * b + 6 * a * b ^ 2 + 2 * b ^ 3|

State before:
a✝ b✝ c : ℤθ
a b : ℤ
⊢ |{ f := a, g := -b, h := 0 }.f ^ 3 - 2 * { f := a, g := -b, h := 0 }.g ^ 3 + 4 * { f := a, g := -b, h := 0 }.h ^ 3 -
                    3 * { f := a, g := -b, h := 0 }.f ^ 2 * { f := a, g := -b, h := 0 }.g -
                  3 * { f := a, g := -b, h := 0 }.f ^ 2 * { f := a, g := -b, h := 0 }.h +
                6 * { f := a, g := -b, h := 0 }.f * { f := a, g := -b, h := 0 }.g ^ 2 +
              6 * { f := a, g := -b, h := 0 }.g ^ 2 * { f := a, g := -b, h := 0 }.h +
            24 * { f := a, g := -b, h := 0 }.f * { f := a, g := -b, h := 0 }.h ^ 2 -
          12 * { f := a, g := -b, h := 0 }.g * { f := a, g := -b, h := 0 }.h ^ 2 -
        12 * { f := a, g := -b, h := 0 }.f * { f := a, g := -b, h := 0 }.g * { f := a, g := -b, h := 0 }.h| =
    |a ^ 3 + 3 * a ^ 2 * b + 6 * a * b ^ 2 + 2 * b ^ 3|
Tactic:
ring_nf
State after:
no goals