EI002A

eisenstein_adjoint_product_is_norm_scale

Alpha v34 independently verified · alpha_closed; checked-use authorized; not Stable

The Eisenstein adjugate identity conjugate(a)*(a*b)=N(a)*b follows from checked coordinate associativity and the actual conjugate product.

Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved. Exact original first-admission records.

Exact expanded first-order arithmetic statement

forall a b c d e f g h N. (((((((((a) * (a))) + (((b) * (b))))) + (((((c) * (c))) + (((d) * (d))))))) + (((((a) * (d))) + (((b) * (c)))))) = ((((((((((a) * (b))) + (((b) * (a))))) + (((((c) * (d))) + (((d) * (c))))))) + (((((a) * (c))) + (((b) * (d))))))) + (N))) -> (((((((((((((a) + (d))) * (((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))))) + (((((b) + (c))) * (((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))))))) + (((((d) * (((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))))) + (((c) * (((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))))))))) + (((N) * (f)))) = ((((N) * (e))) + (((((((((a) + (d))) * (((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))))) + (((((b) + (c))) * (((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))))))) + (((((d) * (((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))))) + (((c) * (((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))))))))))) /\ (((((((((((((a) + (d))) * (((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))))) + (((((b) + (c))) * (((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))))))) + (((((d) * (((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))))) + (((c) * (((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))))))))) + (((((d) * (((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))))) + (((c) * (((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))))))))) + (((N) * (h)))) = ((((N) * (g))) + (((((((((((a) + (d))) * (((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))))) + (((((b) + (c))) * (((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))))))) + (((((d) * (((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))))) + (((c) * (((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))))))))) + (((((d) * (((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))))) + (((c) * (((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h)))))))))))))))))

Constructive proof overview

Generated structural guide

The Eisenstein adjugate identity conjugate(a)*(a*b)=N(a)*b follows from checked coordinate associativity and the actual conjugate product.

The unchanged tactic script uses 7 declared prerequisites and contains 97 exact native proof lines.

Alpha v34 checked-use · first admitted v28 · independently kernel and Lean verified; not Stable

Proof neighborhood

Direct dependencies

gaussian_equal_transitive Alpha theorem; checked-use authorized gaussian_equal_symmetric Alpha theorem; checked-use authorized EI0026 eisenstein_product_associate EI0023 eisenstein_product_integer_congruence EI0028 eisenstein_conjugate_product_is_norm gaussian_equal_reflexive Alpha theorem; checked-use authorized EI0029 eisenstein_natural_scalar_product

Direct dependents

EI002B eisenstein_residual_conjugate_identity

Formal native tactic body

Dependencies are introduced as named hypotheses before line 1. Local theorem links identify exact declared prerequisites. This exact body belongs to a complete independently kernel-checked constructive proof bundle and has Alpha checked-use authority; it does not imply Stable membership.

Read the argument

Proof checkpoints

97 script commands · 11 reading checkpoints · 2 local claims

This is a reading aid, not a new proof or a proof-tree certificate. Checkpoint groups are consecutive commands, not inferred branch boundaries. Every step links to the preserved script.

Named ingredients (4)
eisenstein product associateeisenstein product integer congruenceeisenstein conjugate product is normeisenstein natural scalar product

Long local formulas use this family’s existing definitions. Each new abbreviation was expanded back to the identical native formula, including its free-variable context. The original edition is preserved below.

01Fix variables and assumptionsL1–10

Work with arbitrary variables or the premises of the current implication.

  1. L1
    intro a
  2. L2
    intro b
  3. L3
    intro c
  4. L4
    intro d
  5. L5
    intro e
  6. L6
    intro f
  7. L7
    intro g
  8. L8
    intro h
  9. L9
    intro N
  10. L10
    intro hnorm
02Establish hassociationL11–20

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply gaussian equal symmetric.

  1. L11
    have hassociation · expand full local formula (1,488 characters)have hassociation : EisensteinCoordinateProduct(a + d,b + c,d,c,a · e + b · f + (c · h + d · g),a · f + b · e + (c · g + d · h),a · g + b · h + (c · e + d · f) + (c · h + d · g),a · h + b · g + (c · f + d · e) + (c · g + d · h),((a + d) · a + (b + c) · b + (d · d + c · c)) · e + ((a + d) · b + (b + c) · a + (d · c + c · d)) · f + (((a + d) · c + (b + c) · d + (d · a + c · b) + (d · d + c · c)) · h + ((a + d) · d + (b + c) · c + (d · b + c · a) + (d · c + c · d)) · g),((a + d) · a + (b + c) · b + (d · d + c · c)) · f + ((a + d) · b + (b + c) · a + (d · c + c · d)) · e + (((a + d) · c + (b + c) · d + (d · a + c · b) + (d · d + c · c)) · g + ((a + d) · d + (b + c) · c + (d · b + c · a) + (d · c + c · d)) · h),((a + d) · a + (b + c) · b + (d · d + c · c)) · g + ((a + d) · b + (b + c) · a + (d · c + c · d)) · h + (((a + d) · c + (b + c) · d + (d · a + c · b) + (d · d + c · c)) · e + ((a + d) · d + (b + c) · c + (d · b + c · a) + (d · c + c · d)) · f) + (((a + d) · c + (b + c) · d + (d · a + c · b) + (d · d + c · c)) · h + ((a + d) · d + (b + c) · c + (d · b + c · a) + (d · c + c · d)) · g),((a + d) · a + (b + c) · b + (d · d + c · c)) · h + ((a + d) · b + (b + c) · a + (d · c + c · d)) · g + (((a + d) · c + (b + c) · d + (d · a + c · b) + (d · d + c · c)) · f + ((a + d) · d + (b + c) · c + (d · b + c · a) + (d · c + c · d)) · e) + (((a + d) · c + (b + c) · d + (d · a + c · b) + (d · d + c · c)) · g + ((a + d) · d + (b + c) · c + (d · b + c · a) + (d · c + c · d)) · h))
    Definitions: EisensteinCoordinateProduct
  2. L12
    specialize gaussian_equal_symmetric ((((((((((((((a) + (d))) * (a))) + (((((b) + (c))) * (b))))) + (((((d) * (d))) + (((c) * (c))))))) * (e))) + (((((((((((a) + (d))) * (b))) + (((((b) + (c))) * (a))))) + (((((d) * (c))) + (((c) * (d))))))) * (f))))) + (((((((((((((((a) + (d))) * (c))) + (((((b) + (c))) * (d))))) + (((((d) * (a))) + (((c) * (b))))))) + (((((d) * (d))) + (((c) * (c))))))) * (h))) + (((((((((((((a) + (d))) * (d))) + (((((b) + (c))) * (c))))) + (((((d) * (b))) + (((c) * (a))))))) + (((((d) * (c))) + (((c) * (d))))))) * (g))))))
  3. L13
    specialize gaussian_equal_symmetric ((((((((((((((a) + (d))) * (a))) + (((((b) + (c))) * (b))))) + (((((d) * (d))) + (((c) * (c))))))) * (f))) + (((((((((((a) + (d))) * (b))) + (((((b) + (c))) * (a))))) + (((((d) * (c))) + (((c) * (d))))))) * (e))))) + (((((((((((((((a) + (d))) * (c))) + (((((b) + (c))) * (d))))) + (((((d) * (a))) + (((c) * (b))))))) + (((((d) * (d))) + (((c) * (c))))))) * (g))) + (((((((((((((a) + (d))) * (d))) + (((((b) + (c))) * (c))))) + (((((d) * (b))) + (((c) * (a))))))) + (((((d) * (c))) + (((c) * (d))))))) * (h))))))
  4. L14
    specialize gaussian_equal_symmetric ((((((((((((((((a) + (d))) * (a))) + (((((b) + (c))) * (b))))) + (((((d) * · expand full local formula (847 characters)specialize gaussian_equal_symmetric ((((((((((((((((a) + (d))) * (a))) + (((((b) + (c))) * (b))))) + (((((d) * (d))) + (((c) * (c))))))) * (g))) + (((((((((((a) + (d))) * (b))) + (((((b) + (c))) * (a))))) + (((((d) * (c))) + (((c) * (d))))))) * (h))))) + (((((((((((((((a) + (d))) * (c))) + (((((b) + (c))) * (d))))) + (((((d) * (a))) + (((c) * (b))))))) + (((((d) * (d))) + (((c) * (c))))))) * (e))) + (((((((((((((a) + (d))) * (d))) + (((((b) + (c))) * (c))))) + (((((d) * (b))) + (((c) * (a))))))) + (((((d) * (c))) + (((c) * (d))))))) * (f))))))) + (((((((((((((((a) + (d))) * (c))) + (((((b) + (c))) * (d))))) + (((((d) * (a))) + (((c) * (b))))))) + (((((d) * (d))) + (((c) * (c))))))) * (h))) + (((((((((((((a) + (d))) * (d))) + (((((b) + (c))) * (c))))) + (((((d) * (b))) + (((c) * (a))))))) + (((((d) * (c))) + (((c) * (d))))))) * (g))))))
  5. L15
    specialize gaussian_equal_symmetric ((((((((((((((((a) + (d))) * (a))) + (((((b) + (c))) * (b))))) + (((((d) * · expand full local formula (847 characters)specialize gaussian_equal_symmetric ((((((((((((((((a) + (d))) * (a))) + (((((b) + (c))) * (b))))) + (((((d) * (d))) + (((c) * (c))))))) * (h))) + (((((((((((a) + (d))) * (b))) + (((((b) + (c))) * (a))))) + (((((d) * (c))) + (((c) * (d))))))) * (g))))) + (((((((((((((((a) + (d))) * (c))) + (((((b) + (c))) * (d))))) + (((((d) * (a))) + (((c) * (b))))))) + (((((d) * (d))) + (((c) * (c))))))) * (f))) + (((((((((((((a) + (d))) * (d))) + (((((b) + (c))) * (c))))) + (((((d) * (b))) + (((c) * (a))))))) + (((((d) * (c))) + (((c) * (d))))))) * (e))))))) + (((((((((((((((a) + (d))) * (c))) + (((((b) + (c))) * (d))))) + (((((d) * (a))) + (((c) * (b))))))) + (((((d) * (d))) + (((c) * (c))))))) * (g))) + (((((((((((((a) + (d))) * (d))) + (((((b) + (c))) * (c))))) + (((((d) * (b))) + (((c) * (a))))))) + (((((d) * (c))) + (((c) * (d))))))) * (h))))))
  6. L16
    specialize gaussian_equal_symmetric ((((((((a) + (d))) * (((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))))) + (((((b) + (c))) * (((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))))))) + (((((d) * (((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))))) + (((c) * (((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))))))))
  7. L17
    specialize gaussian_equal_symmetric ((((((((a) + (d))) * (((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))))) + (((((b) + (c))) * (((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))))))) + (((((d) * (((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))))) + (((c) * (((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))))))))
  8. L18
    specialize gaussian_equal_symmetric ((((((((((a) + (d))) * (((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e · expand full local formula (747 characters)specialize gaussian_equal_symmetric ((((((((((a) + (d))) * (((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))))) + (((((b) + (c))) * (((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))))))) + (((((d) * (((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))))) + (((c) * (((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))))))))) + (((((d) * (((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))))) + (((c) * (((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))))))))
  9. L19
    specialize gaussian_equal_symmetric ((((((((((a) + (d))) * (((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f · expand full local formula (747 characters)specialize gaussian_equal_symmetric ((((((((((a) + (d))) * (((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))))) + (((((b) + (c))) * (((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))))))) + (((((d) * (((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))))) + (((c) * (((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))))))))) + (((((d) * (((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))))) + (((c) * (((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))))))))
  10. L20
    apply gaussian_equal_symmetric
03Use earlier factsL21–30

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L21
    specialize eisenstein_product_associate ((a) + (d))
  2. L22
    specialize eisenstein_product_associate ((b) + (c))
  3. L23
    specialize eisenstein_product_associate d
  4. L24
    specialize eisenstein_product_associate c
  5. L25
    specialize eisenstein_product_associate a
  6. L26
    specialize eisenstein_product_associate b
  7. L27
    specialize eisenstein_product_associate c
  8. L28
    specialize eisenstein_product_associate d
  9. L29
    specialize eisenstein_product_associate e
  10. L30
    specialize eisenstein_product_associate f
04Use earlier factsL31–33

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L31
    specialize eisenstein_product_associate g
  2. L32
    specialize eisenstein_product_associate h
  3. L33
    apply eisenstein_product_associate
05Establish hscalingL34–43

Establish this local claim before using it. It is not an additional assumption.

  1. L34
    have hscaling : EisensteinCoordinateProduct((a + d) · a + (b + c) · b + (d · d + c · c),(a + d) · b + (b + c) · a + (d · c + c · d),(a + d) · c + (b + c) · d + (d · a + c · b) + (d · d + c · c),(a + d) · d + (b + c) · c + (d · b + c · a) + (d · c + c · d),e,f,g,h,N · e,N · f,N · g,N · h)Definitions: EisensteinCoordinateProduct
  2. L35
    specialize gaussian_equal_transitive ((((((((((((((a) + (d))) * (a))) + (((((b) + (c))) * (b))))) + (((((d) * (d))) + (((c) * (c))))))) * (e))) + (((((((((((a) + (d))) * (b))) + (((((b) + (c))) * (a))))) + (((((d) * (c))) + (((c) * (d))))))) * (f))))) + (((((((((((((((a) + (d))) * (c))) + (((((b) + (c))) * (d))))) + (((((d) * (a))) + (((c) * (b))))))) + (((((d) * (d))) + (((c) * (c))))))) * (h))) + (((((((((((((a) + (d))) * (d))) + (((((b) + (c))) * (c))))) + (((((d) * (b))) + (((c) * (a))))))) + (((((d) * (c))) + (((c) * (d))))))) * (g))))))
  3. L36
    specialize gaussian_equal_transitive ((((((((((((((a) + (d))) * (a))) + (((((b) + (c))) * (b))))) + (((((d) * (d))) + (((c) * (c))))))) * (f))) + (((((((((((a) + (d))) * (b))) + (((((b) + (c))) * (a))))) + (((((d) * (c))) + (((c) * (d))))))) * (e))))) + (((((((((((((((a) + (d))) * (c))) + (((((b) + (c))) * (d))))) + (((((d) * (a))) + (((c) * (b))))))) + (((((d) * (d))) + (((c) * (c))))))) * (g))) + (((((((((((((a) + (d))) * (d))) + (((((b) + (c))) * (c))))) + (((((d) * (b))) + (((c) * (a))))))) + (((((d) * (c))) + (((c) * (d))))))) * (h))))))
  4. L37
    specialize gaussian_equal_transitive ((((((((((((((((a) + (d))) * (a))) + (((((b) + (c))) * (b))))) + (((((d) * · expand full local formula (848 characters)specialize gaussian_equal_transitive ((((((((((((((((a) + (d))) * (a))) + (((((b) + (c))) * (b))))) + (((((d) * (d))) + (((c) * (c))))))) * (g))) + (((((((((((a) + (d))) * (b))) + (((((b) + (c))) * (a))))) + (((((d) * (c))) + (((c) * (d))))))) * (h))))) + (((((((((((((((a) + (d))) * (c))) + (((((b) + (c))) * (d))))) + (((((d) * (a))) + (((c) * (b))))))) + (((((d) * (d))) + (((c) * (c))))))) * (e))) + (((((((((((((a) + (d))) * (d))) + (((((b) + (c))) * (c))))) + (((((d) * (b))) + (((c) * (a))))))) + (((((d) * (c))) + (((c) * (d))))))) * (f))))))) + (((((((((((((((a) + (d))) * (c))) + (((((b) + (c))) * (d))))) + (((((d) * (a))) + (((c) * (b))))))) + (((((d) * (d))) + (((c) * (c))))))) * (h))) + (((((((((((((a) + (d))) * (d))) + (((((b) + (c))) * (c))))) + (((((d) * (b))) + (((c) * (a))))))) + (((((d) * (c))) + (((c) * (d))))))) * (g))))))
  5. L38
    specialize gaussian_equal_transitive ((((((((((((((((a) + (d))) * (a))) + (((((b) + (c))) * (b))))) + (((((d) * · expand full local formula (848 characters)specialize gaussian_equal_transitive ((((((((((((((((a) + (d))) * (a))) + (((((b) + (c))) * (b))))) + (((((d) * (d))) + (((c) * (c))))))) * (h))) + (((((((((((a) + (d))) * (b))) + (((((b) + (c))) * (a))))) + (((((d) * (c))) + (((c) * (d))))))) * (g))))) + (((((((((((((((a) + (d))) * (c))) + (((((b) + (c))) * (d))))) + (((((d) * (a))) + (((c) * (b))))))) + (((((d) * (d))) + (((c) * (c))))))) * (f))) + (((((((((((((a) + (d))) * (d))) + (((((b) + (c))) * (c))))) + (((((d) * (b))) + (((c) * (a))))))) + (((((d) * (c))) + (((c) * (d))))))) * (e))))))) + (((((((((((((((a) + (d))) * (c))) + (((((b) + (c))) * (d))))) + (((((d) * (a))) + (((c) * (b))))))) + (((((d) * (d))) + (((c) * (c))))))) * (g))) + (((((((((((((a) + (d))) * (d))) + (((((b) + (c))) * (c))))) + (((((d) * (b))) + (((c) * (a))))))) + (((((d) * (c))) + (((c) * (d))))))) * (h))))))
  6. L39
    specialize gaussian_equal_transitive ((((((N) * (e))) + (((0) * (f))))) + (((((0) * (h))) + (((0) * (g))))))
  7. L40
    specialize gaussian_equal_transitive ((((((N) * (f))) + (((0) * (e))))) + (((((0) * (g))) + (((0) * (h))))))
  8. L41
    specialize gaussian_equal_transitive ((((((((N) * (g))) + (((0) * (h))))) + (((((0) * (e))) + (((0) * (f))))))) + (((((0) * (h))) + (((0) * (g))))))
  9. L42
    specialize gaussian_equal_transitive ((((((((N) * (h))) + (((0) * (g))))) + (((((0) * (f))) + (((0) * (e))))))) + (((((0) * (g))) + (((0) * (h))))))
  10. L43
    specialize gaussian_equal_transitive ((N) * (e))
06Use earlier factsL44–53

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L44
    specialize gaussian_equal_transitive ((N) * (f))
  2. L45
    specialize gaussian_equal_transitive ((N) * (g))
  3. L46
    specialize gaussian_equal_transitive ((N) * (h))
  4. L47
    apply gaussian_equal_transitive
  5. L48
    specialize eisenstein_product_integer_congruence ((((((((a) + (d))) * (a))) + (((((b) + (c))) * (b))))) + (((((d) * (d))) + (((c) * (c))))))
  6. L49
    specialize eisenstein_product_integer_congruence ((((((((a) + (d))) * (b))) + (((((b) + (c))) * (a))))) + (((((d) * (c))) + (((c) * (d))))))
  7. L50
    specialize eisenstein_product_integer_congruence ((((((((((a) + (d))) * (c))) + (((((b) + (c))) * (d))))) + (((((d) * (a))) + (((c) * (b))))))) + (((((d) * (d))) + (((c) * (c))))))
  8. L51
    specialize eisenstein_product_integer_congruence ((((((((((a) + (d))) * (d))) + (((((b) + (c))) * (c))))) + (((((d) * (b))) + (((c) * (a))))))) + (((((d) * (c))) + (((c) * (d))))))
  9. L52
    specialize eisenstein_product_integer_congruence N
  10. L53
    specialize eisenstein_product_integer_congruence 0
07Use earlier factsL54–63

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L54
    specialize eisenstein_product_integer_congruence 0
  2. L55
    specialize eisenstein_product_integer_congruence 0
  3. L56
    specialize eisenstein_product_integer_congruence e
  4. L57
    specialize eisenstein_product_integer_congruence f
  5. L58
    specialize eisenstein_product_integer_congruence g
  6. L59
    specialize eisenstein_product_integer_congruence h
  7. L60
    specialize eisenstein_product_integer_congruence e
  8. L61
    specialize eisenstein_product_integer_congruence f
  9. L62
    specialize eisenstein_product_integer_congruence g
  10. L63
    specialize eisenstein_product_integer_congruence h
08Use earlier factsL64–73

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L64
    apply eisenstein_product_integer_congruence
  2. L65
    specialize eisenstein_conjugate_product_is_norm a
  3. L66
    specialize eisenstein_conjugate_product_is_norm b
  4. L67
    specialize eisenstein_conjugate_product_is_norm c
  5. L68
    specialize eisenstein_conjugate_product_is_norm d
  6. L69
    specialize eisenstein_conjugate_product_is_norm N
  7. L70
    apply eisenstein_conjugate_product_is_norm
  8. L71
    exact hnorm
  9. L72
    specialize gaussian_equal_reflexive e
  10. L73
    specialize gaussian_equal_reflexive f
09Use earlier factsL74–83

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L74
    specialize gaussian_equal_reflexive g
  2. L75
    specialize gaussian_equal_reflexive h
  3. L76
    apply gaussian_equal_reflexive
  4. L77
    specialize eisenstein_natural_scalar_product N
  5. L78
    specialize eisenstein_natural_scalar_product e
  6. L79
    specialize eisenstein_natural_scalar_product f
  7. L80
    specialize eisenstein_natural_scalar_product g
  8. L81
    specialize eisenstein_natural_scalar_product h
  9. L82
    apply eisenstein_natural_scalar_product
  10. L83
    specialize gaussian_equal_transitive ((((((((a) + (d))) * (((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))))) + (((((b) + (c))) * (((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))))))) + (((((d) * (((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))))) + (((c) * (((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))))))))
10Use earlier factsL84–93

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L84
    specialize gaussian_equal_transitive ((((((((a) + (d))) * (((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))))) + (((((b) + (c))) * (((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))))))) + (((((d) * (((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))))) + (((c) * (((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))))))))
  2. L85
    specialize gaussian_equal_transitive ((((((((((a) + (d))) * (((((((((a) * (g))) + (((b) * (h))))) + (((((c) * ( · expand full local formula (748 characters)specialize gaussian_equal_transitive ((((((((((a) + (d))) * (((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))))) + (((((b) + (c))) * (((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))))))) + (((((d) * (((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))))) + (((c) * (((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))))))))) + (((((d) * (((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))))) + (((c) * (((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))))))))
  3. L86
    specialize gaussian_equal_transitive ((((((((((a) + (d))) * (((((((((a) * (h))) + (((b) * (g))))) + (((((c) * ( · expand full local formula (748 characters)specialize gaussian_equal_transitive ((((((((((a) + (d))) * (((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))))) + (((((b) + (c))) * (((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))))))) + (((((d) * (((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))))) + (((c) * (((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))))))))) + (((((d) * (((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))))) + (((c) * (((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))))))))
  4. L87
    specialize gaussian_equal_transitive ((((((((((((((a) + (d))) * (a))) + (((((b) + (c))) * (b))))) + (((((d) * (d))) + (((c) * (c))))))) * (e))) + (((((((((((a) + (d))) * (b))) + (((((b) + (c))) * (a))))) + (((((d) * (c))) + (((c) * (d))))))) * (f))))) + (((((((((((((((a) + (d))) * (c))) + (((((b) + (c))) * (d))))) + (((((d) * (a))) + (((c) * (b))))))) + (((((d) * (d))) + (((c) * (c))))))) * (h))) + (((((((((((((a) + (d))) * (d))) + (((((b) + (c))) * (c))))) + (((((d) * (b))) + (((c) * (a))))))) + (((((d) * (c))) + (((c) * (d))))))) * (g))))))
  5. L88
    specialize gaussian_equal_transitive ((((((((((((((a) + (d))) * (a))) + (((((b) + (c))) * (b))))) + (((((d) * (d))) + (((c) * (c))))))) * (f))) + (((((((((((a) + (d))) * (b))) + (((((b) + (c))) * (a))))) + (((((d) * (c))) + (((c) * (d))))))) * (e))))) + (((((((((((((((a) + (d))) * (c))) + (((((b) + (c))) * (d))))) + (((((d) * (a))) + (((c) * (b))))))) + (((((d) * (d))) + (((c) * (c))))))) * (g))) + (((((((((((((a) + (d))) * (d))) + (((((b) + (c))) * (c))))) + (((((d) * (b))) + (((c) * (a))))))) + (((((d) * (c))) + (((c) * (d))))))) * (h))))))
  6. L89
    specialize gaussian_equal_transitive ((((((((((((((((a) + (d))) * (a))) + (((((b) + (c))) * (b))))) + (((((d) * · expand full local formula (848 characters)specialize gaussian_equal_transitive ((((((((((((((((a) + (d))) * (a))) + (((((b) + (c))) * (b))))) + (((((d) * (d))) + (((c) * (c))))))) * (g))) + (((((((((((a) + (d))) * (b))) + (((((b) + (c))) * (a))))) + (((((d) * (c))) + (((c) * (d))))))) * (h))))) + (((((((((((((((a) + (d))) * (c))) + (((((b) + (c))) * (d))))) + (((((d) * (a))) + (((c) * (b))))))) + (((((d) * (d))) + (((c) * (c))))))) * (e))) + (((((((((((((a) + (d))) * (d))) + (((((b) + (c))) * (c))))) + (((((d) * (b))) + (((c) * (a))))))) + (((((d) * (c))) + (((c) * (d))))))) * (f))))))) + (((((((((((((((a) + (d))) * (c))) + (((((b) + (c))) * (d))))) + (((((d) * (a))) + (((c) * (b))))))) + (((((d) * (d))) + (((c) * (c))))))) * (h))) + (((((((((((((a) + (d))) * (d))) + (((((b) + (c))) * (c))))) + (((((d) * (b))) + (((c) * (a))))))) + (((((d) * (c))) + (((c) * (d))))))) * (g))))))
  7. L90
    specialize gaussian_equal_transitive ((((((((((((((((a) + (d))) * (a))) + (((((b) + (c))) * (b))))) + (((((d) * · expand full local formula (848 characters)specialize gaussian_equal_transitive ((((((((((((((((a) + (d))) * (a))) + (((((b) + (c))) * (b))))) + (((((d) * (d))) + (((c) * (c))))))) * (h))) + (((((((((((a) + (d))) * (b))) + (((((b) + (c))) * (a))))) + (((((d) * (c))) + (((c) * (d))))))) * (g))))) + (((((((((((((((a) + (d))) * (c))) + (((((b) + (c))) * (d))))) + (((((d) * (a))) + (((c) * (b))))))) + (((((d) * (d))) + (((c) * (c))))))) * (f))) + (((((((((((((a) + (d))) * (d))) + (((((b) + (c))) * (c))))) + (((((d) * (b))) + (((c) * (a))))))) + (((((d) * (c))) + (((c) * (d))))))) * (e))))))) + (((((((((((((((a) + (d))) * (c))) + (((((b) + (c))) * (d))))) + (((((d) * (a))) + (((c) * (b))))))) + (((((d) * (d))) + (((c) * (c))))))) * (g))) + (((((((((((((a) + (d))) * (d))) + (((((b) + (c))) * (c))))) + (((((d) * (b))) + (((c) * (a))))))) + (((((d) * (c))) + (((c) * (d))))))) * (h))))))
  8. L91
    specialize gaussian_equal_transitive ((N) * (e))
  9. L92
    specialize gaussian_equal_transitive ((N) * (f))
  10. L93
    specialize gaussian_equal_transitive ((N) * (g))
11Use earlier factsL94–97

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L94
    specialize gaussian_equal_transitive ((N) * (h))
  2. L95
    apply gaussian_equal_transitive
  3. L96
    exact hassociation
  4. L97
    exact hscaling

Library-wide reading audit

Original exact command ledger · 97 lines
  1. 0001intro a
  2. 0002intro b
  3. 0003intro c
  4. 0004intro d
  5. 0005intro e
  6. 0006intro f
  7. 0007intro g
  8. 0008intro h
  9. 0009intro N
  10. 0010intro hnorm
  11. 0011have hassociation : ((((((((((((a) + (d))) * (((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))))) + (((((b) + (c))) * (((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))))))) + (((((d) * (((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))))) + (((c) * (((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))))))))) + (((((((((((((((a) + (d))) * (a))) + (((((b) + (c))) * (b))))) + (((((d) * (d))) + (((c) * (c))))))) * (f))) + (((((((((((a) + (d))) * (b))) + (((((b) + (c))) * (a))))) + (((((d) * (c))) + (((c) * (d))))))) * (e))))) + (((((((((((((((a) + (d))) * (c))) + (((((b) + (c))) * (d))))) + (((((d) * (a))) + (((c) * (b))))))) + (((((d) * (d))) + (((c) * (c))))))) * (g))) + (((((((((((((a) + (d))) * (d))) + (((((b) + (c))) * (c))))) + (((((d) * (b))) + (((c) * (a))))))) + (((((d) * (c))) + (((c) * (d))))))) * (h)))))))) = ((((((((((((((((a) + (d))) * (a))) + (((((b) + (c))) * (b))))) + (((((d) * (d))) + (((c) * (c))))))) * (e))) + (((((((((((a) + (d))) * (b))) + (((((b) + (c))) * (a))))) + (((((d) * (c))) + (((c) * (d))))))) * (f))))) + (((((((((((((((a) + (d))) * (c))) + (((((b) + (c))) * (d))))) + (((((d) * (a))) + (((c) * (b))))))) + (((((d) * (d))) + (((c) * (c))))))) * (h))) + (((((((((((((a) + (d))) * (d))) + (((((b) + (c))) * (c))))) + (((((d) * (b))) + (((c) * (a))))))) + (((((d) * (c))) + (((c) * (d))))))) * (g))))))) + (((((((((a) + (d))) * (((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))))) + (((((b) + (c))) * (((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))))))) + (((((d) * (((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))))) + (((c) * (((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))))))))))) /\ (((((((((((((a) + (d))) * (((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))))) + (((((b) + (c))) * (((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))))))) + (((((d) * (((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))))) + (((c) * (((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))))))))) + (((((d) * (((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))))) + (((c) * (((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))))))))) + (((((((((((((((((a) + (d))) * (a))) + (((((b) + (c))) * (b))))) + (((((d) * (d))) + (((c) * (c))))))) * (h))) + (((((((((((a) + (d))) * (b))) + (((((b) + (c))) * (a))))) + (((((d) * (c))) + (((c) * (d))))))) * (g))))) + (((((((((((((((a) + (d))) * (c))) + (((((b) + (c))) * (d))))) + (((((d) * (a))) + (((c) * (b))))))) + (((((d) * (d))) + (((c) * (c))))))) * (f))) + (((((((((((((a) + (d))) * (d))) + (((((b) + (c))) * (c))))) + (((((d) * (b))) + (((c) * (a))))))) + (((((d) * (c))) + (((c) * (d))))))) * (e))))))) + (((((((((((((((a) + (d))) * (c))) + (((((b) + (c))) * (d))))) + (((((d) * (a))) + (((c) * (b))))))) + (((((d) * (d))) + (((c) * (c))))))) * (g))) + (((((((((((((a) + (d))) * (d))) + (((((b) + (c))) * (c))))) + (((((d) * (b))) + (((c) * (a))))))) + (((((d) * (c))) + (((c) * (d))))))) * (h)))))))) = ((((((((((((((((((a) + (d))) * (a))) + (((((b) + (c))) * (b))))) + (((((d) * (d))) + (((c) * (c))))))) * (g))) + (((((((((((a) + (d))) * (b))) + (((((b) + (c))) * (a))))) + (((((d) * (c))) + (((c) * (d))))))) * (h))))) + (((((((((((((((a) + (d))) * (c))) + (((((b) + (c))) * (d))))) + (((((d) * (a))) + (((c) * (b))))))) + (((((d) * (d))) + (((c) * (c))))))) * (e))) + (((((((((((((a) + (d))) * (d))) + (((((b) + (c))) * (c))))) + (((((d) * (b))) + (((c) * (a))))))) + (((((d) * (c))) + (((c) * (d))))))) * (f))))))) + (((((((((((((((a) + (d))) * (c))) + (((((b) + (c))) * (d))))) + (((((d) * (a))) + (((c) * (b))))))) + (((((d) * (d))) + (((c) * (c))))))) * (h))) + (((((((((((((a) + (d))) * (d))) + (((((b) + (c))) * (c))))) + (((((d) * (b))) + (((c) * (a))))))) + (((((d) * (c))) + (((c) * (d))))))) * (g))))))) + (((((((((((a) + (d))) * (((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))))) + (((((b) + (c))) * (((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))))))) + (((((d) * (((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))))) + (((c) * (((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))))))))) + (((((d) * (((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))))) + (((c) * (((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))))))))))))
  12. 0012specialize gaussian_equal_symmetric ((((((((((((((a) + (d))) * (a))) + (((((b) + (c))) * (b))))) + (((((d) * (d))) + (((c) * (c))))))) * (e))) + (((((((((((a) + (d))) * (b))) + (((((b) + (c))) * (a))))) + (((((d) * (c))) + (((c) * (d))))))) * (f))))) + (((((((((((((((a) + (d))) * (c))) + (((((b) + (c))) * (d))))) + (((((d) * (a))) + (((c) * (b))))))) + (((((d) * (d))) + (((c) * (c))))))) * (h))) + (((((((((((((a) + (d))) * (d))) + (((((b) + (c))) * (c))))) + (((((d) * (b))) + (((c) * (a))))))) + (((((d) * (c))) + (((c) * (d))))))) * (g))))))
  13. 0013specialize gaussian_equal_symmetric ((((((((((((((a) + (d))) * (a))) + (((((b) + (c))) * (b))))) + (((((d) * (d))) + (((c) * (c))))))) * (f))) + (((((((((((a) + (d))) * (b))) + (((((b) + (c))) * (a))))) + (((((d) * (c))) + (((c) * (d))))))) * (e))))) + (((((((((((((((a) + (d))) * (c))) + (((((b) + (c))) * (d))))) + (((((d) * (a))) + (((c) * (b))))))) + (((((d) * (d))) + (((c) * (c))))))) * (g))) + (((((((((((((a) + (d))) * (d))) + (((((b) + (c))) * (c))))) + (((((d) * (b))) + (((c) * (a))))))) + (((((d) * (c))) + (((c) * (d))))))) * (h))))))
  14. 0014specialize gaussian_equal_symmetric ((((((((((((((((a) + (d))) * (a))) + (((((b) + (c))) * (b))))) + (((((d) * (d))) + (((c) * (c))))))) * (g))) + (((((((((((a) + (d))) * (b))) + (((((b) + (c))) * (a))))) + (((((d) * (c))) + (((c) * (d))))))) * (h))))) + (((((((((((((((a) + (d))) * (c))) + (((((b) + (c))) * (d))))) + (((((d) * (a))) + (((c) * (b))))))) + (((((d) * (d))) + (((c) * (c))))))) * (e))) + (((((((((((((a) + (d))) * (d))) + (((((b) + (c))) * (c))))) + (((((d) * (b))) + (((c) * (a))))))) + (((((d) * (c))) + (((c) * (d))))))) * (f))))))) + (((((((((((((((a) + (d))) * (c))) + (((((b) + (c))) * (d))))) + (((((d) * (a))) + (((c) * (b))))))) + (((((d) * (d))) + (((c) * (c))))))) * (h))) + (((((((((((((a) + (d))) * (d))) + (((((b) + (c))) * (c))))) + (((((d) * (b))) + (((c) * (a))))))) + (((((d) * (c))) + (((c) * (d))))))) * (g))))))
  15. 0015specialize gaussian_equal_symmetric ((((((((((((((((a) + (d))) * (a))) + (((((b) + (c))) * (b))))) + (((((d) * (d))) + (((c) * (c))))))) * (h))) + (((((((((((a) + (d))) * (b))) + (((((b) + (c))) * (a))))) + (((((d) * (c))) + (((c) * (d))))))) * (g))))) + (((((((((((((((a) + (d))) * (c))) + (((((b) + (c))) * (d))))) + (((((d) * (a))) + (((c) * (b))))))) + (((((d) * (d))) + (((c) * (c))))))) * (f))) + (((((((((((((a) + (d))) * (d))) + (((((b) + (c))) * (c))))) + (((((d) * (b))) + (((c) * (a))))))) + (((((d) * (c))) + (((c) * (d))))))) * (e))))))) + (((((((((((((((a) + (d))) * (c))) + (((((b) + (c))) * (d))))) + (((((d) * (a))) + (((c) * (b))))))) + (((((d) * (d))) + (((c) * (c))))))) * (g))) + (((((((((((((a) + (d))) * (d))) + (((((b) + (c))) * (c))))) + (((((d) * (b))) + (((c) * (a))))))) + (((((d) * (c))) + (((c) * (d))))))) * (h))))))
  16. 0016specialize gaussian_equal_symmetric ((((((((a) + (d))) * (((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))))) + (((((b) + (c))) * (((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))))))) + (((((d) * (((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))))) + (((c) * (((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))))))))
  17. 0017specialize gaussian_equal_symmetric ((((((((a) + (d))) * (((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))))) + (((((b) + (c))) * (((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))))))) + (((((d) * (((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))))) + (((c) * (((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))))))))
  18. 0018specialize gaussian_equal_symmetric ((((((((((a) + (d))) * (((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))))) + (((((b) + (c))) * (((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))))))) + (((((d) * (((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))))) + (((c) * (((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))))))))) + (((((d) * (((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))))) + (((c) * (((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))))))))
  19. 0019specialize gaussian_equal_symmetric ((((((((((a) + (d))) * (((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))))) + (((((b) + (c))) * (((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))))))) + (((((d) * (((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))))) + (((c) * (((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))))))))) + (((((d) * (((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))))) + (((c) * (((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))))))))
  20. 0020apply gaussian_equal_symmetric
  21. 0021specialize eisenstein_product_associate ((a) + (d))
  22. 0022specialize eisenstein_product_associate ((b) + (c))
  23. 0023specialize eisenstein_product_associate d
  24. 0024specialize eisenstein_product_associate c
  25. 0025specialize eisenstein_product_associate a
  26. 0026specialize eisenstein_product_associate b
  27. 0027specialize eisenstein_product_associate c
  28. 0028specialize eisenstein_product_associate d
  29. 0029specialize eisenstein_product_associate e
  30. 0030specialize eisenstein_product_associate f
  31. 0031specialize eisenstein_product_associate g
  32. 0032specialize eisenstein_product_associate h
  33. 0033apply eisenstein_product_associate
  34. 0034have hscaling : ((((((((((((((((((a) + (d))) * (a))) + (((((b) + (c))) * (b))))) + (((((d) * (d))) + (((c) * (c))))))) * (e))) + (((((((((((a) + (d))) * (b))) + (((((b) + (c))) * (a))))) + (((((d) * (c))) + (((c) * (d))))))) * (f))))) + (((((((((((((((a) + (d))) * (c))) + (((((b) + (c))) * (d))))) + (((((d) * (a))) + (((c) * (b))))))) + (((((d) * (d))) + (((c) * (c))))))) * (h))) + (((((((((((((a) + (d))) * (d))) + (((((b) + (c))) * (c))))) + (((((d) * (b))) + (((c) * (a))))))) + (((((d) * (c))) + (((c) * (d))))))) * (g))))))) + (((N) * (f)))) = ((((N) * (e))) + (((((((((((((((a) + (d))) * (a))) + (((((b) + (c))) * (b))))) + (((((d) * (d))) + (((c) * (c))))))) * (f))) + (((((((((((a) + (d))) * (b))) + (((((b) + (c))) * (a))))) + (((((d) * (c))) + (((c) * (d))))))) * (e))))) + (((((((((((((((a) + (d))) * (c))) + (((((b) + (c))) * (d))))) + (((((d) * (a))) + (((c) * (b))))))) + (((((d) * (d))) + (((c) * (c))))))) * (g))) + (((((((((((((a) + (d))) * (d))) + (((((b) + (c))) * (c))))) + (((((d) * (b))) + (((c) * (a))))))) + (((((d) * (c))) + (((c) * (d))))))) * (h))))))))) /\ (((((((((((((((((((a) + (d))) * (a))) + (((((b) + (c))) * (b))))) + (((((d) * (d))) + (((c) * (c))))))) * (g))) + (((((((((((a) + (d))) * (b))) + (((((b) + (c))) * (a))))) + (((((d) * (c))) + (((c) * (d))))))) * (h))))) + (((((((((((((((a) + (d))) * (c))) + (((((b) + (c))) * (d))))) + (((((d) * (a))) + (((c) * (b))))))) + (((((d) * (d))) + (((c) * (c))))))) * (e))) + (((((((((((((a) + (d))) * (d))) + (((((b) + (c))) * (c))))) + (((((d) * (b))) + (((c) * (a))))))) + (((((d) * (c))) + (((c) * (d))))))) * (f))))))) + (((((((((((((((a) + (d))) * (c))) + (((((b) + (c))) * (d))))) + (((((d) * (a))) + (((c) * (b))))))) + (((((d) * (d))) + (((c) * (c))))))) * (h))) + (((((((((((((a) + (d))) * (d))) + (((((b) + (c))) * (c))))) + (((((d) * (b))) + (((c) * (a))))))) + (((((d) * (c))) + (((c) * (d))))))) * (g))))))) + (((N) * (h)))) = ((((N) * (g))) + (((((((((((((((((a) + (d))) * (a))) + (((((b) + (c))) * (b))))) + (((((d) * (d))) + (((c) * (c))))))) * (h))) + (((((((((((a) + (d))) * (b))) + (((((b) + (c))) * (a))))) + (((((d) * (c))) + (((c) * (d))))))) * (g))))) + (((((((((((((((a) + (d))) * (c))) + (((((b) + (c))) * (d))))) + (((((d) * (a))) + (((c) * (b))))))) + (((((d) * (d))) + (((c) * (c))))))) * (f))) + (((((((((((((a) + (d))) * (d))) + (((((b) + (c))) * (c))))) + (((((d) * (b))) + (((c) * (a))))))) + (((((d) * (c))) + (((c) * (d))))))) * (e))))))) + (((((((((((((((a) + (d))) * (c))) + (((((b) + (c))) * (d))))) + (((((d) * (a))) + (((c) * (b))))))) + (((((d) * (d))) + (((c) * (c))))))) * (g))) + (((((((((((((a) + (d))) * (d))) + (((((b) + (c))) * (c))))) + (((((d) * (b))) + (((c) * (a))))))) + (((((d) * (c))) + (((c) * (d))))))) * (h))))))))))
  35. 0035specialize gaussian_equal_transitive ((((((((((((((a) + (d))) * (a))) + (((((b) + (c))) * (b))))) + (((((d) * (d))) + (((c) * (c))))))) * (e))) + (((((((((((a) + (d))) * (b))) + (((((b) + (c))) * (a))))) + (((((d) * (c))) + (((c) * (d))))))) * (f))))) + (((((((((((((((a) + (d))) * (c))) + (((((b) + (c))) * (d))))) + (((((d) * (a))) + (((c) * (b))))))) + (((((d) * (d))) + (((c) * (c))))))) * (h))) + (((((((((((((a) + (d))) * (d))) + (((((b) + (c))) * (c))))) + (((((d) * (b))) + (((c) * (a))))))) + (((((d) * (c))) + (((c) * (d))))))) * (g))))))
  36. 0036specialize gaussian_equal_transitive ((((((((((((((a) + (d))) * (a))) + (((((b) + (c))) * (b))))) + (((((d) * (d))) + (((c) * (c))))))) * (f))) + (((((((((((a) + (d))) * (b))) + (((((b) + (c))) * (a))))) + (((((d) * (c))) + (((c) * (d))))))) * (e))))) + (((((((((((((((a) + (d))) * (c))) + (((((b) + (c))) * (d))))) + (((((d) * (a))) + (((c) * (b))))))) + (((((d) * (d))) + (((c) * (c))))))) * (g))) + (((((((((((((a) + (d))) * (d))) + (((((b) + (c))) * (c))))) + (((((d) * (b))) + (((c) * (a))))))) + (((((d) * (c))) + (((c) * (d))))))) * (h))))))
  37. 0037specialize gaussian_equal_transitive ((((((((((((((((a) + (d))) * (a))) + (((((b) + (c))) * (b))))) + (((((d) * (d))) + (((c) * (c))))))) * (g))) + (((((((((((a) + (d))) * (b))) + (((((b) + (c))) * (a))))) + (((((d) * (c))) + (((c) * (d))))))) * (h))))) + (((((((((((((((a) + (d))) * (c))) + (((((b) + (c))) * (d))))) + (((((d) * (a))) + (((c) * (b))))))) + (((((d) * (d))) + (((c) * (c))))))) * (e))) + (((((((((((((a) + (d))) * (d))) + (((((b) + (c))) * (c))))) + (((((d) * (b))) + (((c) * (a))))))) + (((((d) * (c))) + (((c) * (d))))))) * (f))))))) + (((((((((((((((a) + (d))) * (c))) + (((((b) + (c))) * (d))))) + (((((d) * (a))) + (((c) * (b))))))) + (((((d) * (d))) + (((c) * (c))))))) * (h))) + (((((((((((((a) + (d))) * (d))) + (((((b) + (c))) * (c))))) + (((((d) * (b))) + (((c) * (a))))))) + (((((d) * (c))) + (((c) * (d))))))) * (g))))))
  38. 0038specialize gaussian_equal_transitive ((((((((((((((((a) + (d))) * (a))) + (((((b) + (c))) * (b))))) + (((((d) * (d))) + (((c) * (c))))))) * (h))) + (((((((((((a) + (d))) * (b))) + (((((b) + (c))) * (a))))) + (((((d) * (c))) + (((c) * (d))))))) * (g))))) + (((((((((((((((a) + (d))) * (c))) + (((((b) + (c))) * (d))))) + (((((d) * (a))) + (((c) * (b))))))) + (((((d) * (d))) + (((c) * (c))))))) * (f))) + (((((((((((((a) + (d))) * (d))) + (((((b) + (c))) * (c))))) + (((((d) * (b))) + (((c) * (a))))))) + (((((d) * (c))) + (((c) * (d))))))) * (e))))))) + (((((((((((((((a) + (d))) * (c))) + (((((b) + (c))) * (d))))) + (((((d) * (a))) + (((c) * (b))))))) + (((((d) * (d))) + (((c) * (c))))))) * (g))) + (((((((((((((a) + (d))) * (d))) + (((((b) + (c))) * (c))))) + (((((d) * (b))) + (((c) * (a))))))) + (((((d) * (c))) + (((c) * (d))))))) * (h))))))
  39. 0039specialize gaussian_equal_transitive ((((((N) * (e))) + (((0) * (f))))) + (((((0) * (h))) + (((0) * (g))))))
  40. 0040specialize gaussian_equal_transitive ((((((N) * (f))) + (((0) * (e))))) + (((((0) * (g))) + (((0) * (h))))))
  41. 0041specialize gaussian_equal_transitive ((((((((N) * (g))) + (((0) * (h))))) + (((((0) * (e))) + (((0) * (f))))))) + (((((0) * (h))) + (((0) * (g))))))
  42. 0042specialize gaussian_equal_transitive ((((((((N) * (h))) + (((0) * (g))))) + (((((0) * (f))) + (((0) * (e))))))) + (((((0) * (g))) + (((0) * (h))))))
  43. 0043specialize gaussian_equal_transitive ((N) * (e))
  44. 0044specialize gaussian_equal_transitive ((N) * (f))
  45. 0045specialize gaussian_equal_transitive ((N) * (g))
  46. 0046specialize gaussian_equal_transitive ((N) * (h))
  47. 0047apply gaussian_equal_transitive
  48. 0048specialize eisenstein_product_integer_congruence ((((((((a) + (d))) * (a))) + (((((b) + (c))) * (b))))) + (((((d) * (d))) + (((c) * (c))))))
  49. 0049specialize eisenstein_product_integer_congruence ((((((((a) + (d))) * (b))) + (((((b) + (c))) * (a))))) + (((((d) * (c))) + (((c) * (d))))))
  50. 0050specialize eisenstein_product_integer_congruence ((((((((((a) + (d))) * (c))) + (((((b) + (c))) * (d))))) + (((((d) * (a))) + (((c) * (b))))))) + (((((d) * (d))) + (((c) * (c))))))
  51. 0051specialize eisenstein_product_integer_congruence ((((((((((a) + (d))) * (d))) + (((((b) + (c))) * (c))))) + (((((d) * (b))) + (((c) * (a))))))) + (((((d) * (c))) + (((c) * (d))))))
  52. 0052specialize eisenstein_product_integer_congruence N
  53. 0053specialize eisenstein_product_integer_congruence 0
  54. 0054specialize eisenstein_product_integer_congruence 0
  55. 0055specialize eisenstein_product_integer_congruence 0
  56. 0056specialize eisenstein_product_integer_congruence e
  57. 0057specialize eisenstein_product_integer_congruence f
  58. 0058specialize eisenstein_product_integer_congruence g
  59. 0059specialize eisenstein_product_integer_congruence h
  60. 0060specialize eisenstein_product_integer_congruence e
  61. 0061specialize eisenstein_product_integer_congruence f
  62. 0062specialize eisenstein_product_integer_congruence g
  63. 0063specialize eisenstein_product_integer_congruence h
  64. 0064apply eisenstein_product_integer_congruence
  65. 0065specialize eisenstein_conjugate_product_is_norm a
  66. 0066specialize eisenstein_conjugate_product_is_norm b
  67. 0067specialize eisenstein_conjugate_product_is_norm c
  68. 0068specialize eisenstein_conjugate_product_is_norm d
  69. 0069specialize eisenstein_conjugate_product_is_norm N
  70. 0070apply eisenstein_conjugate_product_is_norm
  71. 0071exact hnorm
  72. 0072specialize gaussian_equal_reflexive e
  73. 0073specialize gaussian_equal_reflexive f
  74. 0074specialize gaussian_equal_reflexive g
  75. 0075specialize gaussian_equal_reflexive h
  76. 0076apply gaussian_equal_reflexive
  77. 0077specialize eisenstein_natural_scalar_product N
  78. 0078specialize eisenstein_natural_scalar_product e
  79. 0079specialize eisenstein_natural_scalar_product f
  80. 0080specialize eisenstein_natural_scalar_product g
  81. 0081specialize eisenstein_natural_scalar_product h
  82. 0082apply eisenstein_natural_scalar_product
  83. 0083specialize gaussian_equal_transitive ((((((((a) + (d))) * (((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))))) + (((((b) + (c))) * (((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))))))) + (((((d) * (((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))))) + (((c) * (((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))))))))
  84. 0084specialize gaussian_equal_transitive ((((((((a) + (d))) * (((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))))) + (((((b) + (c))) * (((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))))))) + (((((d) * (((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))))) + (((c) * (((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))))))))
  85. 0085specialize gaussian_equal_transitive ((((((((((a) + (d))) * (((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))))) + (((((b) + (c))) * (((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))))))) + (((((d) * (((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))))) + (((c) * (((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))))))))) + (((((d) * (((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))))) + (((c) * (((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))))))))
  86. 0086specialize gaussian_equal_transitive ((((((((((a) + (d))) * (((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))))) + (((((b) + (c))) * (((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))))))) + (((((d) * (((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))))) + (((c) * (((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))))))))) + (((((d) * (((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))))) + (((c) * (((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))))))))
  87. 0087specialize gaussian_equal_transitive ((((((((((((((a) + (d))) * (a))) + (((((b) + (c))) * (b))))) + (((((d) * (d))) + (((c) * (c))))))) * (e))) + (((((((((((a) + (d))) * (b))) + (((((b) + (c))) * (a))))) + (((((d) * (c))) + (((c) * (d))))))) * (f))))) + (((((((((((((((a) + (d))) * (c))) + (((((b) + (c))) * (d))))) + (((((d) * (a))) + (((c) * (b))))))) + (((((d) * (d))) + (((c) * (c))))))) * (h))) + (((((((((((((a) + (d))) * (d))) + (((((b) + (c))) * (c))))) + (((((d) * (b))) + (((c) * (a))))))) + (((((d) * (c))) + (((c) * (d))))))) * (g))))))
  88. 0088specialize gaussian_equal_transitive ((((((((((((((a) + (d))) * (a))) + (((((b) + (c))) * (b))))) + (((((d) * (d))) + (((c) * (c))))))) * (f))) + (((((((((((a) + (d))) * (b))) + (((((b) + (c))) * (a))))) + (((((d) * (c))) + (((c) * (d))))))) * (e))))) + (((((((((((((((a) + (d))) * (c))) + (((((b) + (c))) * (d))))) + (((((d) * (a))) + (((c) * (b))))))) + (((((d) * (d))) + (((c) * (c))))))) * (g))) + (((((((((((((a) + (d))) * (d))) + (((((b) + (c))) * (c))))) + (((((d) * (b))) + (((c) * (a))))))) + (((((d) * (c))) + (((c) * (d))))))) * (h))))))
  89. 0089specialize gaussian_equal_transitive ((((((((((((((((a) + (d))) * (a))) + (((((b) + (c))) * (b))))) + (((((d) * (d))) + (((c) * (c))))))) * (g))) + (((((((((((a) + (d))) * (b))) + (((((b) + (c))) * (a))))) + (((((d) * (c))) + (((c) * (d))))))) * (h))))) + (((((((((((((((a) + (d))) * (c))) + (((((b) + (c))) * (d))))) + (((((d) * (a))) + (((c) * (b))))))) + (((((d) * (d))) + (((c) * (c))))))) * (e))) + (((((((((((((a) + (d))) * (d))) + (((((b) + (c))) * (c))))) + (((((d) * (b))) + (((c) * (a))))))) + (((((d) * (c))) + (((c) * (d))))))) * (f))))))) + (((((((((((((((a) + (d))) * (c))) + (((((b) + (c))) * (d))))) + (((((d) * (a))) + (((c) * (b))))))) + (((((d) * (d))) + (((c) * (c))))))) * (h))) + (((((((((((((a) + (d))) * (d))) + (((((b) + (c))) * (c))))) + (((((d) * (b))) + (((c) * (a))))))) + (((((d) * (c))) + (((c) * (d))))))) * (g))))))
  90. 0090specialize gaussian_equal_transitive ((((((((((((((((a) + (d))) * (a))) + (((((b) + (c))) * (b))))) + (((((d) * (d))) + (((c) * (c))))))) * (h))) + (((((((((((a) + (d))) * (b))) + (((((b) + (c))) * (a))))) + (((((d) * (c))) + (((c) * (d))))))) * (g))))) + (((((((((((((((a) + (d))) * (c))) + (((((b) + (c))) * (d))))) + (((((d) * (a))) + (((c) * (b))))))) + (((((d) * (d))) + (((c) * (c))))))) * (f))) + (((((((((((((a) + (d))) * (d))) + (((((b) + (c))) * (c))))) + (((((d) * (b))) + (((c) * (a))))))) + (((((d) * (c))) + (((c) * (d))))))) * (e))))))) + (((((((((((((((a) + (d))) * (c))) + (((((b) + (c))) * (d))))) + (((((d) * (a))) + (((c) * (b))))))) + (((((d) * (d))) + (((c) * (c))))))) * (g))) + (((((((((((((a) + (d))) * (d))) + (((((b) + (c))) * (c))))) + (((((d) * (b))) + (((c) * (a))))))) + (((((d) * (c))) + (((c) * (d))))))) * (h))))))
  91. 0091specialize gaussian_equal_transitive ((N) * (e))
  92. 0092specialize gaussian_equal_transitive ((N) * (f))
  93. 0093specialize gaussian_equal_transitive ((N) * (g))
  94. 0094specialize gaussian_equal_transitive ((N) * (h))
  95. 0095apply gaussian_equal_transitive
  96. 0096exact hassociation
  97. 0097exact hscaling