CubicPrelim.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Characteristic-polynomial reduction for the cubic classification in §3.

theorem OAI.MUB6.characteristic_polynomial_expansion line 13

theorem OAI.MUB6.characteristic_polynomial_in_cubes line 26

Source documentation

Unit entries with first and second power sums zero have a characteristic polynomial depending only on X³, as used at the start of cubic classification.

theorem characteristic_polynomial_in_cubes (v : (Fin 6) → ℂ)
    (hv : ∀ i, Complex.normSq (v i) = 1)
    (h1 : ∑ i, v i = 0) (h2 : ∑ i, v i ^ 2 = 0) :
    (∏ i, (Polynomial.X - Polynomial.C (v i))) =
      Polynomial.X ^ 6 - Polynomial.C (elementarySum v 3) * Polynomial.X ^ 3 +
        Polynomial.C (∏ i, v i) := by
…

Mentions: OAI.MUB6.elementarySum

theorem OAI.MUB6.cubed_entry_quadratic line 39
theorem OAI.MUB6.quadratic_two_values line 55

theorem OAI.MUB6.cube_values_at_most_two line 69

Source documentation

This gives the first, algebraic part of the two-triples conclusion. The multiplicity statement is a separate obligation.

theorem cube_values_at_most_two (v : (Fin 6) → ℂ)
    (hv : ∀ i, Complex.normSq (v i) = 1)
    (h1 : ∑ i, v i = 0) (h2 : ∑ i, v i ^ 2 = 0) :
    ∃ a b : ℂ, ∀ i, v i ^ 3 = a ∨ v i ^ 3 = b := by
…