CubicMultiplicityCore.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Multiplicity counting once the two possible cubed values are known.

theorem OAI.MUB6.unit_cube_mul_conj_square line 12
def OAI.MUB6.cubeClass line 18
theorem OAI.MUB6.same_cube_zero_sum_card_ge_three line 25
Source documentation
A nonempty zero-sum collection of nonzero numbers with the same cube has at least three members: one term cannot vanish, and two opposite terms have opposite cubes.
```
theorem same_cube_zero_sum_card_ge_three (v : (Fin 6) → ℂ) (s : Finset (Fin 6))
    (a : ℂ) (ha : a ≠ 0) (hne : s.Nonempty)
    (hcube : ∀ i ∈ s, v i ^ 3 = a) (hsum : ∑ i ∈ s, v i = 0) :
    3 ≤ s.card := by
…
```
theorem OAI.MUB6.two_cube_classes_card_three line 50