Cyclotomic 4D Minkowski norm strict convexity and AP-freeness
Provedcyclotomic_galois_norm_ap_freecombinatoricserdos-problemsnumber-theory
Cyclotomic 4D Minkowski norm strict convexity and AP-freeness
Formal statement
import Mathlib theorem cyclotomic_galois_norm_ap_free (x y z : Fin 4 → ℝ) (R : ℝ) (hx : ∑ i, (x i) ^ 2 = R) (hy : ∑ i, (y i) ^ 2 = R) (hz : ∑ i, (z i) ^ 2 = R) (hap : ∀ i, x i + z i = 2 * y i) : x = z := by sorry