FormalConjectures.Paper.CasasAlvero

/-
Copyright 2025 The Formal Conjectures Authors.

Licensed under the Apache License, Version 2.0 (the "License");
you may not use this file except in compliance with the License.
You may obtain a copy of the License at

    https://www.apache.org/licenses/LICENSE-2.0

Unless required by applicable law or agreed to in writing, software
distributed under the License is distributed on an "AS IS" BASIS,
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
See the License for the specific language governing permissions and
limitations under the License.
-/
module

public import FormalConjecturesUtil

Casas-Alvero Conjecture

References:

The Casas-Alvero conjecture for infinitely many degrees

MathOverflow

The Casas-Alvero conjecture states that if a univariate polynomial P of degree d over a field of characteristic zero shares a non-trivial factor with its Hasse derivatives up to order d-1, then P must be of the form (X - α)ᵈ for some α in the field.

The conjecture has been proven for:

Degrees d ≤ 8

Degrees of the form p^k where p is prime

Degrees of the form 2p^k where p is prime

The conjecture is false in positive characteristic p for polynomials of degree p+1.

The conjecture is now claimed to be proven in this paper:

Proof of the Casas-Alvero conjecture: Soham Ghosh)

@[expose] public sectionnamespace CasasAlveroopen Polynomialvariable {K L : Type*} [Field K] [Field L] {f : K →+* L}

A polynomial P satisfies the Casas-Alvero property if it shares a factor with each of its Hasse derivatives up to order d-1, where d is the degree of P.

def HasCasasAlveroProp (P : K[X]) : Prop :=
  ∀ i ∈ Finset.range P.natDegree, ¬ IsCoprime P (P.hasseDeriv i)

A stronger version of the Casas-Alvero property, which requires that the polynomial P shares a root with each of its Hasse derivatives up to order deg P - 1. The subscript r indicates "root" in the definition.

def HasCasasAlveroPropᵣ (P : K[X]) : Prop :=
  ∀ i ∈ Finset.range P.natDegree, ∃ α : K, IsRoot P α ∧ IsRoot (P.hasseDeriv i) α

@[category API, AMS 12]
theorem HasCasasAlveroPropᵣ.hasCasasAlveroProp {P : K[X]}
    (hca : HasCasasAlveroPropᵣ P) : HasCasasAlveroProp P := byK:Type u_1inst✝:Field KP:K[X]hca:HasCasasAlveroPropᵣ P⊢ HasCasasAlveroProp P
  intro i hi coprimeK:Type u_1inst✝:Field KP:K[X]hca:HasCasasAlveroPropᵣ Pi:ℕhi:i ∈ Finset.range P.natDegreecoprime:IsCoprime P ((hasseDeriv i) P)⊢ False
  simp_rw [K:Type u_1inst✝:Field KP:K[X]hca:HasCasasAlveroPropᵣ Pi:ℕhi:i ∈ Finset.range P.natDegreecoprime:IsCoprime P ((hasseDeriv i) P)⊢ FalseHasCasasAlveroPropᵣ,K:Type u_1inst✝:Field KP:K[X]hca:∀ i ∈ Finset.range P.natDegree, ∃ α, P.IsRoot α ∧ ((hasseDeriv i) P).IsRoot αi:ℕhi:i ∈ Finset.range P.natDegreecoprime:IsCoprime P ((hasseDeriv i) P)⊢ False ← dvd_iff_isRootK:Type u_1inst✝:Field KP:K[X]i:ℕhi:i ∈ Finset.range P.natDegreecoprime:IsCoprime P ((hasseDeriv i) P)hca:∀ i ∈ Finset.range P.natDegree, ∃ α, X - C α ∣ P ∧ X - C α ∣ (hasseDeriv i) P⊢ False] at hca
  have ⟨α, hα, hαi⟩ := hca i hiK:Type u_1inst✝:Field KP:K[X]i:ℕhi:i ∈ Finset.range P.natDegreecoprime:IsCoprime P ((hasseDeriv i) P)hca:∀ i ∈ Finset.range P.natDegree, ∃ α, X - C α ∣ P ∧ X - C α ∣ (hasseDeriv i) Pα:Khα:X - C α ∣ Phαi:X - C α ∣ (hasseDeriv i) P⊢ False
  exact not_isUnit_X_sub_C _ (coprime.isUnit_of_dvd' hα hαi)All goals completed! 🐙

@[category API, AMS 12]
theorem HasCasasAlveroProp.map_iff {P : K[X]} :
    HasCasasAlveroProp (P.map f) ↔ HasCasasAlveroProp P := byK:Type u_1L:Type u_2inst✝¹:Field Kinst✝:Field Lf:K →+* LP:K[X]⊢ HasCasasAlveroProp (map f P) ↔ HasCasasAlveroProp P
  simp [HasCasasAlveroProp, P.natDegree_map f, hasseDeriv_map, isCoprime_map]All goals completed! 🐙

@[category API, AMS 12]
theorem hasCasasAlveroProp_iffᵣ {P : K[X]} [IsAlgClosed K] :
    HasCasasAlveroProp P ↔ HasCasasAlveroPropᵣ P := byK:Type u_1inst✝¹:Field KP:K[X]inst✝:IsAlgClosed K⊢ HasCasasAlveroProp P ↔ HasCasasAlveroPropᵣ P
  refine ⟨?_, HasCasasAlveroPropᵣ.hasCasasAlveroProp⟩K:Type u_1inst✝¹:Field KP:K[X]inst✝:IsAlgClosed K⊢ HasCasasAlveroProp P → HasCasasAlveroPropᵣ P
  simp_rw [K:Type u_1inst✝¹:Field KP:K[X]inst✝:IsAlgClosed K⊢ HasCasasAlveroProp P → HasCasasAlveroPropᵣ PHasCasasAlveroProp,K:Type u_1inst✝¹:Field KP:K[X]inst✝:IsAlgClosed K⊢ (∀ i ∈ Finset.range P.natDegree, ¬IsCoprime P ((hasseDeriv i) P)) → HasCasasAlveroPropᵣ P HasCasasAlveroPropᵣ,K:Type u_1inst✝¹:Field KP:K[X]inst✝:IsAlgClosed K⊢ (∀ i ∈ Finset.range P.natDegree, ¬IsCoprime P ((hasseDeriv i) P)) →
  ∀ i ∈ Finset.range P.natDegree, ∃ α, P.IsRoot α ∧ ((hasseDeriv i) P).IsRoot α
    isCoprime_iff_aeval_ne_zero_of_isAlgClosed K K,K:Type u_1inst✝¹:Field KP:K[X]inst✝:IsAlgClosed K⊢ (∀ i ∈ Finset.range P.natDegree, ¬∀ (a : K), (aeval a) P ≠ 0 ∨ (aeval a) ((hasseDeriv i) P) ≠ 0) →
  ∀ i ∈ Finset.range P.natDegree, ∃ α, P.IsRoot α ∧ ((hasseDeriv i) P).IsRoot α coe_aeval_eq_evalK:Type u_1inst✝¹:Field KP:K[X]inst✝:IsAlgClosed K⊢ (∀ i ∈ Finset.range P.natDegree, ¬∀ (a : K), eval a P ≠ 0 ∨ eval a ((hasseDeriv i) P) ≠ 0) →
  ∀ i ∈ Finset.range P.natDegree, ∃ α, P.IsRoot α ∧ ((hasseDeriv i) P).IsRoot α]
  push NotK:Type u_1inst✝¹:Field KP:K[X]inst✝:IsAlgClosed K⊢ (∀ i ∈ Finset.range P.natDegree, ∃ a, eval a P = 0 ∧ eval a ((hasseDeriv i) P) = 0) →
  ∀ i ∈ Finset.range P.natDegree, ∃ α, P.IsRoot α ∧ ((hasseDeriv i) P).IsRoot α
  exact (· · ·)All goals completed! 🐙

universe u in

Note that whether we use HasCasasAlveroProp or HasCasasAlveroPropᵣ to state the Casas-Alvero conjecture, we obtain the following equivalent statements.


@[category API, AMS 12]
lemma casas_alvero_iffᵣ :
    (∀ {K : Type u} [Field K] [CharZero K] (P : K[X]),
      P.Monic → HasCasasAlveroProp P → ∃ α : K, P = (X - C α) ^ P.natDegree) ↔
    (∀ {K : Type u} [Field K] [CharZero K] (P : K[X]),
      P.Monic → HasCasasAlveroPropᵣ P → ∃ α : K, P = (X - C α) ^ P.natDegree) := by⊢ (∀ {K : Type u} [inst : Field K] [CharZero K] (P : K[X]),
    P.Monic → HasCasasAlveroProp P → ∃ α, P = (X - C α) ^ P.natDegree) ↔
  ∀ {K : Type u} [inst : Field K] [CharZero K] (P : K[X]),
    P.Monic → HasCasasAlveroPropᵣ P → ∃ α, P = (X - C α) ^ P.natDegree
  refine ⟨fun h _ _ _ P hP hca ↦ h P hP hca.hasCasasAlveroProp, fun h K _ _ P hP hca ↦ ?_⟩h:∀ {K : Type u} [inst : Field K] [CharZero K] (P : K[X]),
  P.Monic → HasCasasAlveroPropᵣ P → ∃ α, P = (X - C α) ^ P.natDegreeK:Type ux✝¹:Field Kx✝:CharZero KP:K[X]hP:P.Monichca:HasCasasAlveroProp P⊢ ∃ α, P = (X - C α) ^ P.natDegree
  let L := AlgebraicClosure Kh:∀ {K : Type u} [inst : Field K] [CharZero K] (P : K[X]),
  P.Monic → HasCasasAlveroPropᵣ P → ∃ α, P = (X - C α) ^ P.natDegreeK:Type ux✝¹:Field Kx✝:CharZero KP:K[X]hP:P.Monichca:HasCasasAlveroProp PL:Type u := AlgebraicClosure K⊢ ∃ α, P = (X - C α) ^ P.natDegree
  have ⟨α, eq⟩ := h (P.map (algebraMap K L)) (hP.map _) <|
    hasCasasAlveroProp_iffᵣ.mp <| HasCasasAlveroProp.map_iff.mpr hcah:∀ {K : Type u} [inst : Field K] [CharZero K] (P : K[X]),
  P.Monic → HasCasasAlveroPropᵣ P → ∃ α, P = (X - C α) ^ P.natDegreeK:Type ux✝¹:Field Kx✝:CharZero KP:K[X]hP:P.Monichca:HasCasasAlveroProp PL:Type u := AlgebraicClosure Kα:Leq:map (algebraMap K L) P = (X - C α) ^ (map (algebraMap K L) P).natDegree⊢ ∃ α, P = (X - C α) ^ P.natDegree
  by_cases h0 : P.natDegree = 0posh:∀ {K : Type u} [inst : Field K] [CharZero K] (P : K[X]),
  P.Monic → HasCasasAlveroPropᵣ P → ∃ α, P = (X - C α) ^ P.natDegreeK:Type ux✝¹:Field Kx✝:CharZero KP:K[X]hP:P.Monichca:HasCasasAlveroProp PL:Type u := AlgebraicClosure Kα:Leq:map (algebraMap K L) P = (X - C α) ^ (map (algebraMap K L) P).natDegreeh0:P.natDegree = 0⊢ ∃ α, P = (X - C α) ^ P.natDegreenegh:∀ {K : Type u} [inst : Field K] [CharZero K] (P : K[X]),
  P.Monic → HasCasasAlveroPropᵣ P → ∃ α, P = (X - C α) ^ P.natDegreeK:Type ux✝¹:Field Kx✝:CharZero KP:K[X]hP:P.Monichca:HasCasasAlveroProp PL:Type u := AlgebraicClosure Kα:Leq:map (algebraMap K L) P = (X - C α) ^ (map (algebraMap K L) P).natDegreeh0:¬P.natDegree = 0⊢ ∃ α, P = (X - C α) ^ P.natDegree
  ·posh:∀ {K : Type u} [inst : Field K] [CharZero K] (P : K[X]),
  P.Monic → HasCasasAlveroPropᵣ P → ∃ α, P = (X - C α) ^ P.natDegreeK:Type ux✝¹:Field Kx✝:CharZero KP:K[X]hP:P.Monichca:HasCasasAlveroProp PL:Type u := AlgebraicClosure Kα:Leq:map (algebraMap K L) P = (X - C α) ^ (map (algebraMap K L) P).natDegreeh0:P.natDegree = 0⊢ ∃ α, P = (X - C α) ^ P.natDegree simp [hP.natDegree_eq_zero.mp h0]All goals completed! 🐙
  let α' := - P.nextCoeff / P.natDegreenegh:∀ {K : Type u} [inst : Field K] [CharZero K] (P : K[X]),
  P.Monic → HasCasasAlveroPropᵣ P → ∃ α, P = (X - C α) ^ P.natDegreeK:Type ux✝¹:Field Kx✝:CharZero KP:K[X]hP:P.Monichca:HasCasasAlveroProp PL:Type u := AlgebraicClosure Kα:Leq:map (algebraMap K L) P = (X - C α) ^ (map (algebraMap K L) P).natDegreeh0:¬P.natDegree = 0α':K := -P.nextCoeff / ↑P.natDegree⊢ ∃ α, P = (X - C α) ^ P.natDegree
  have : algebraMap K L α' = α := by⊢ (∀ {K : Type u} [inst : Field K] [CharZero K] (P : K[X]),
    P.Monic → HasCasasAlveroProp P → ∃ α, P = (X - C α) ^ P.natDegree) ↔
  ∀ {K : Type u} [inst : Field K] [CharZero K] (P : K[X]),
    P.Monic → HasCasasAlveroPropᵣ P → ∃ α, P = (X - C α) ^ P.natDegreenegh:∀ {K : Type u} [inst : Field K] [CharZero K] (P : K[X]),
  P.Monic → HasCasasAlveroPropᵣ P → ∃ α, P = (X - C α) ^ P.natDegreeK:Type ux✝¹:Field Kx✝:CharZero KP:K[X]hP:P.Monichca:HasCasasAlveroProp PL:Type u := AlgebraicClosure Kα:Leq:map (algebraMap K L) P = (X - C α) ^ (map (algebraMap K L) P).natDegreeh0:¬P.natDegree = 0α':K := -P.nextCoeff / ↑P.natDegreethis:(algebraMap K L) α' = α⊢ ∃ α, P = (X - C α) ^ P.natDegree
    simp_rw [h:∀ {K : Type u} [inst : Field K] [CharZero K] (P : K[X]),
  P.Monic → HasCasasAlveroPropᵣ P → ∃ α, P = (X - C α) ^ P.natDegreeK:Type ux✝¹:Field Kx✝:CharZero KP:K[X]hP:P.Monichca:HasCasasAlveroProp PL:Type u := AlgebraicClosure Kα:Leq:map (algebraMap K L) P = (X - C α) ^ (map (algebraMap K L) P).natDegreeh0:¬P.natDegree = 0α':K := -P.nextCoeff / ↑P.natDegree⊢ (algebraMap K L) α' = αnegh:∀ {K : Type u} [inst : Field K] [CharZero K] (P : K[X]),
  P.Monic → HasCasasAlveroPropᵣ P → ∃ α, P = (X - C α) ^ P.natDegreeK:Type ux✝¹:Field Kx✝:CharZero KP:K[X]hP:P.Monichca:HasCasasAlveroProp PL:Type u := AlgebraicClosure Kα:Leq:map (algebraMap K L) P = (X - C α) ^ (map (algebraMap K L) P).natDegreeh0:¬P.natDegree = 0α':K := -P.nextCoeff / ↑P.natDegreethis:(algebraMap K L) α' = α⊢ ∃ α, P = (X - C α) ^ P.natDegreeα',h:∀ {K : Type u} [inst : Field K] [CharZero K] (P : K[X]),
  P.Monic → HasCasasAlveroPropᵣ P → ∃ α, P = (X - C α) ^ P.natDegreeK:Type ux✝¹:Field Kx✝:CharZero KP:K[X]hP:P.Monichca:HasCasasAlveroProp PL:Type u := AlgebraicClosure Kα:Leq:map (algebraMap K L) P = (X - C α) ^ (map (algebraMap K L) P).natDegreeh0:¬P.natDegree = 0α':K := -P.nextCoeff / ↑P.natDegree⊢ (algebraMap K L) (-P.nextCoeff / ↑P.natDegree) = αnegh:∀ {K : Type u} [inst : Field K] [CharZero K] (P : K[X]),
  P.Monic → HasCasasAlveroPropᵣ P → ∃ α, P = (X - C α) ^ P.natDegreeK:Type ux✝¹:Field Kx✝:CharZero KP:K[X]hP:P.Monichca:HasCasasAlveroProp PL:Type u := AlgebraicClosure Kα:Leq:map (algebraMap K L) P = (X - C α) ^ (map (algebraMap K L) P).natDegreeh0:¬P.natDegree = 0α':K := -P.nextCoeff / ↑P.natDegreethis:(algebraMap K L) α' = α⊢ ∃ α, P = (X - C α) ^ P.natDegree div_eq_inv_mul,h:∀ {K : Type u} [inst : Field K] [CharZero K] (P : K[X]),
  P.Monic → HasCasasAlveroPropᵣ P → ∃ α, P = (X - C α) ^ P.natDegreeK:Type ux✝¹:Field Kx✝:CharZero KP:K[X]hP:P.Monichca:HasCasasAlveroProp PL:Type u := AlgebraicClosure Kα:Leq:map (algebraMap K L) P = (X - C α) ^ (map (algebraMap K L) P).natDegreeh0:¬P.natDegree = 0α':K := -P.nextCoeff / ↑P.natDegree⊢ (algebraMap K L) ((↑P.natDegree)⁻¹ * -P.nextCoeff) = αnegh:∀ {K : Type u} [inst : Field K] [CharZero K] (P : K[X]),
  P.Monic → HasCasasAlveroPropᵣ P → ∃ α, P = (X - C α) ^ P.natDegreeK:Type ux✝¹:Field Kx✝:CharZero KP:K[X]hP:P.Monichca:HasCasasAlveroProp PL:Type u := AlgebraicClosure Kα:Leq:map (algebraMap K L) P = (X - C α) ^ (map (algebraMap K L) P).natDegreeh0:¬P.natDegree = 0α':K := -P.nextCoeff / ↑P.natDegreethis:(algebraMap K L) α' = α⊢ ∃ α, P = (X - C α) ^ P.natDegree map_mul,h:∀ {K : Type u} [inst : Field K] [CharZero K] (P : K[X]),
  P.Monic → HasCasasAlveroPropᵣ P → ∃ α, P = (X - C α) ^ P.natDegreeK:Type ux✝¹:Field Kx✝:CharZero KP:K[X]hP:P.Monichca:HasCasasAlveroProp PL:Type u := AlgebraicClosure Kα:Leq:map (algebraMap K L) P = (X - C α) ^ (map (algebraMap K L) P).natDegreeh0:¬P.natDegree = 0α':K := -P.nextCoeff / ↑P.natDegree⊢ (algebraMap K L) (↑P.natDegree)⁻¹ * (algebraMap K L) (-P.nextCoeff) = αnegh:∀ {K : Type u} [inst : Field K] [CharZero K] (P : K[X]),
  P.Monic → HasCasasAlveroPropᵣ P → ∃ α, P = (X - C α) ^ P.natDegreeK:Type ux✝¹:Field Kx✝:CharZero KP:K[X]hP:P.Monichca:HasCasasAlveroProp PL:Type u := AlgebraicClosure Kα:Leq:map (algebraMap K L) P = (X - C α) ^ (map (algebraMap K L) P).natDegreeh0:¬P.natDegree = 0α':K := -P.nextCoeff / ↑P.natDegreethis:(algebraMap K L) α' = α⊢ ∃ α, P = (X - C α) ^ P.natDegree map_neg,h:∀ {K : Type u} [inst : Field K] [CharZero K] (P : K[X]),
  P.Monic → HasCasasAlveroPropᵣ P → ∃ α, P = (X - C α) ^ P.natDegreeK:Type ux✝¹:Field Kx✝:CharZero KP:K[X]hP:P.Monichca:HasCasasAlveroProp PL:Type u := AlgebraicClosure Kα:Leq:map (algebraMap K L) P = (X - C α) ^ (map (algebraMap K L) P).natDegreeh0:¬P.natDegree = 0α':K := -P.nextCoeff / ↑P.natDegree⊢ (algebraMap K L) (↑P.natDegree)⁻¹ * -(algebraMap K L) P.nextCoeff = αnegh:∀ {K : Type u} [inst : Field K] [CharZero K] (P : K[X]),
  P.Monic → HasCasasAlveroPropᵣ P → ∃ α, P = (X - C α) ^ P.natDegreeK:Type ux✝¹:Field Kx✝:CharZero KP:K[X]hP:P.Monichca:HasCasasAlveroProp PL:Type u := AlgebraicClosure Kα:Leq:map (algebraMap K L) P = (X - C α) ^ (map (algebraMap K L) P).natDegreeh0:¬P.natDegree = 0α':K := -P.nextCoeff / ↑P.natDegreethis:(algebraMap K L) α' = α⊢ ∃ α, P = (X - C α) ^ P.natDegree ← nextCoeff_map (algebraMap K L).injective,h:∀ {K : Type u} [inst : Field K] [CharZero K] (P : K[X]),
  P.Monic → HasCasasAlveroPropᵣ P → ∃ α, P = (X - C α) ^ P.natDegreeK:Type ux✝¹:Field Kx✝:CharZero KP:K[X]hP:P.Monichca:HasCasasAlveroProp PL:Type u := AlgebraicClosure Kα:Leq:map (algebraMap K L) P = (X - C α) ^ (map (algebraMap K L) P).natDegreeh0:¬P.natDegree = 0α':K := -P.nextCoeff / ↑P.natDegree⊢ (algebraMap K L) (↑P.natDegree)⁻¹ * -(map (algebraMap K L) P).nextCoeff = αnegh:∀ {K : Type u} [inst : Field K] [CharZero K] (P : K[X]),
  P.Monic → HasCasasAlveroPropᵣ P → ∃ α, P = (X - C α) ^ P.natDegreeK:Type ux✝¹:Field Kx✝:CharZero KP:K[X]hP:P.Monichca:HasCasasAlveroProp PL:Type u := AlgebraicClosure Kα:Leq:map (algebraMap K L) P = (X - C α) ^ (map (algebraMap K L) P).natDegreeh0:¬P.natDegree = 0α':K := -P.nextCoeff / ↑P.natDegreethis:(algebraMap K L) α' = α⊢ ∃ α, P = (X - C α) ^ P.natDegree
      congr_arg nextCoeff eq,h:∀ {K : Type u} [inst : Field K] [CharZero K] (P : K[X]),
  P.Monic → HasCasasAlveroPropᵣ P → ∃ α, P = (X - C α) ^ P.natDegreeK:Type ux✝¹:Field Kx✝:CharZero KP:K[X]hP:P.Monichca:HasCasasAlveroProp PL:Type u := AlgebraicClosure Kα:Leq:map (algebraMap K L) P = (X - C α) ^ (map (algebraMap K L) P).natDegreeh0:¬P.natDegree = 0α':K := -P.nextCoeff / ↑P.natDegree⊢ (algebraMap K L) (↑P.natDegree)⁻¹ * -((X - C α) ^ (map (algebraMap K L) P).natDegree).nextCoeff = αnegh:∀ {K : Type u} [inst : Field K] [CharZero K] (P : K[X]),
  P.Monic → HasCasasAlveroPropᵣ P → ∃ α, P = (X - C α) ^ P.natDegreeK:Type ux✝¹:Field Kx✝:CharZero KP:K[X]hP:P.Monichca:HasCasasAlveroProp PL:Type u := AlgebraicClosure Kα:Leq:map (algebraMap K L) P = (X - C α) ^ (map (algebraMap K L) P).natDegreeh0:¬P.natDegree = 0α':K := -P.nextCoeff / ↑P.natDegreethis:(algebraMap K L) α' = α⊢ ∃ α, P = (X - C α) ^ P.natDegree (monic_X_sub_C α).nextCoeff_pow,h:∀ {K : Type u} [inst : Field K] [CharZero K] (P : K[X]),
  P.Monic → HasCasasAlveroPropᵣ P → ∃ α, P = (X - C α) ^ P.natDegreeK:Type ux✝¹:Field Kx✝:CharZero KP:K[X]hP:P.Monichca:HasCasasAlveroProp PL:Type u := AlgebraicClosure Kα:Leq:map (algebraMap K L) P = (X - C α) ^ (map (algebraMap K L) P).natDegreeh0:¬P.natDegree = 0α':K := -P.nextCoeff / ↑P.natDegree⊢ (algebraMap K L) (↑P.natDegree)⁻¹ * -((map (algebraMap K L) P).natDegree • (X - C α).nextCoeff) = αnegh:∀ {K : Type u} [inst : Field K] [CharZero K] (P : K[X]),
  P.Monic → HasCasasAlveroPropᵣ P → ∃ α, P = (X - C α) ^ P.natDegreeK:Type ux✝¹:Field Kx✝:CharZero KP:K[X]hP:P.Monichca:HasCasasAlveroProp PL:Type u := AlgebraicClosure Kα:Leq:map (algebraMap K L) P = (X - C α) ^ (map (algebraMap K L) P).natDegreeh0:¬P.natDegree = 0α':K := -P.nextCoeff / ↑P.natDegreethis:(algebraMap K L) α' = α⊢ ∃ α, P = (X - C α) ^ P.natDegree nextCoeff_X_sub_C,h:∀ {K : Type u} [inst : Field K] [CharZero K] (P : K[X]),
  P.Monic → HasCasasAlveroPropᵣ P → ∃ α, P = (X - C α) ^ P.natDegreeK:Type ux✝¹:Field Kx✝:CharZero KP:K[X]hP:P.Monichca:HasCasasAlveroProp PL:Type u := AlgebraicClosure Kα:Leq:map (algebraMap K L) P = (X - C α) ^ (map (algebraMap K L) P).natDegreeh0:¬P.natDegree = 0α':K := -P.nextCoeff / ↑P.natDegree⊢ (algebraMap K L) (↑P.natDegree)⁻¹ * -((map (algebraMap K L) P).natDegree • -α) = αnegh:∀ {K : Type u} [inst : Field K] [CharZero K] (P : K[X]),
  P.Monic → HasCasasAlveroPropᵣ P → ∃ α, P = (X - C α) ^ P.natDegreeK:Type ux✝¹:Field Kx✝:CharZero KP:K[X]hP:P.Monichca:HasCasasAlveroProp PL:Type u := AlgebraicClosure Kα:Leq:map (algebraMap K L) P = (X - C α) ^ (map (algebraMap K L) P).natDegreeh0:¬P.natDegree = 0α':K := -P.nextCoeff / ↑P.natDegreethis:(algebraMap K L) α' = α⊢ ∃ α, P = (X - C α) ^ P.natDegree nsmul_eq_mul,h:∀ {K : Type u} [inst : Field K] [CharZero K] (P : K[X]),
  P.Monic → HasCasasAlveroPropᵣ P → ∃ α, P = (X - C α) ^ P.natDegreeK:Type ux✝¹:Field Kx✝:CharZero KP:K[X]hP:P.Monichca:HasCasasAlveroProp PL:Type u := AlgebraicClosure Kα:Leq:map (algebraMap K L) P = (X - C α) ^ (map (algebraMap K L) P).natDegreeh0:¬P.natDegree = 0α':K := -P.nextCoeff / ↑P.natDegree⊢ (algebraMap K L) (↑P.natDegree)⁻¹ * -(↑(map (algebraMap K L) P).natDegree * -α) = αnegh:∀ {K : Type u} [inst : Field K] [CharZero K] (P : K[X]),
  P.Monic → HasCasasAlveroPropᵣ P → ∃ α, P = (X - C α) ^ P.natDegreeK:Type ux✝¹:Field Kx✝:CharZero KP:K[X]hP:P.Monichca:HasCasasAlveroProp PL:Type u := AlgebraicClosure Kα:Leq:map (algebraMap K L) P = (X - C α) ^ (map (algebraMap K L) P).natDegreeh0:¬P.natDegree = 0α':K := -P.nextCoeff / ↑P.natDegreethis:(algebraMap K L) α' = α⊢ ∃ α, P = (X - C α) ^ P.natDegree
      mul_neg _ α,h:∀ {K : Type u} [inst : Field K] [CharZero K] (P : K[X]),
  P.Monic → HasCasasAlveroPropᵣ P → ∃ α, P = (X - C α) ^ P.natDegreeK:Type ux✝¹:Field Kx✝:CharZero KP:K[X]hP:P.Monichca:HasCasasAlveroProp PL:Type u := AlgebraicClosure Kα:Leq:map (algebraMap K L) P = (X - C α) ^ (map (algebraMap K L) P).natDegreeh0:¬P.natDegree = 0α':K := -P.nextCoeff / ↑P.natDegree⊢ (algebraMap K L) (↑P.natDegree)⁻¹ * - -(↑(map (algebraMap K L) P).natDegree * α) = αnegh:∀ {K : Type u} [inst : Field K] [CharZero K] (P : K[X]),
  P.Monic → HasCasasAlveroPropᵣ P → ∃ α, P = (X - C α) ^ P.natDegreeK:Type ux✝¹:Field Kx✝:CharZero KP:K[X]hP:P.Monichca:HasCasasAlveroProp PL:Type u := AlgebraicClosure Kα:Leq:map (algebraMap K L) P = (X - C α) ^ (map (algebraMap K L) P).natDegreeh0:¬P.natDegree = 0α':K := -P.nextCoeff / ↑P.natDegreethis:(algebraMap K L) α' = α⊢ ∃ α, P = (X - C α) ^ P.natDegree neg_neg,h:∀ {K : Type u} [inst : Field K] [CharZero K] (P : K[X]),
  P.Monic → HasCasasAlveroPropᵣ P → ∃ α, P = (X - C α) ^ P.natDegreeK:Type ux✝¹:Field Kx✝:CharZero KP:K[X]hP:P.Monichca:HasCasasAlveroProp PL:Type u := AlgebraicClosure Kα:Leq:map (algebraMap K L) P = (X - C α) ^ (map (algebraMap K L) P).natDegreeh0:¬P.natDegree = 0α':K := -P.nextCoeff / ↑P.natDegree⊢ (algebraMap K L) (↑P.natDegree)⁻¹ * (↑(map (algebraMap K L) P).natDegree * α) = αnegh:∀ {K : Type u} [inst : Field K] [CharZero K] (P : K[X]),
  P.Monic → HasCasasAlveroPropᵣ P → ∃ α, P = (X - C α) ^ P.natDegreeK:Type ux✝¹:Field Kx✝:CharZero KP:K[X]hP:P.Monichca:HasCasasAlveroProp PL:Type u := AlgebraicClosure Kα:Leq:map (algebraMap K L) P = (X - C α) ^ (map (algebraMap K L) P).natDegreeh0:¬P.natDegree = 0α':K := -P.nextCoeff / ↑P.natDegreethis:(algebraMap K L) α' = α⊢ ∃ α, P = (X - C α) ^ P.natDegree ← mul_assoc,h:∀ {K : Type u} [inst : Field K] [CharZero K] (P : K[X]),
  P.Monic → HasCasasAlveroPropᵣ P → ∃ α, P = (X - C α) ^ P.natDegreeK:Type ux✝¹:Field Kx✝:CharZero KP:K[X]hP:P.Monichca:HasCasasAlveroProp PL:Type u := AlgebraicClosure Kα:Leq:map (algebraMap K L) P = (X - C α) ^ (map (algebraMap K L) P).natDegreeh0:¬P.natDegree = 0α':K := -P.nextCoeff / ↑P.natDegree⊢ (algebraMap K L) (↑P.natDegree)⁻¹ * ↑(map (algebraMap K L) P).natDegree * α = αnegh:∀ {K : Type u} [inst : Field K] [CharZero K] (P : K[X]),
  P.Monic → HasCasasAlveroPropᵣ P → ∃ α, P = (X - C α) ^ P.natDegreeK:Type ux✝¹:Field Kx✝:CharZero KP:K[X]hP:P.Monichca:HasCasasAlveroProp PL:Type u := AlgebraicClosure Kα:Leq:map (algebraMap K L) P = (X - C α) ^ (map (algebraMap K L) P).natDegreeh0:¬P.natDegree = 0α':K := -P.nextCoeff / ↑P.natDegreethis:(algebraMap K L) α' = α⊢ ∃ α, P = (X - C α) ^ P.natDegree natDegree_map,h:∀ {K : Type u} [inst : Field K] [CharZero K] (P : K[X]),
  P.Monic → HasCasasAlveroPropᵣ P → ∃ α, P = (X - C α) ^ P.natDegreeK:Type ux✝¹:Field Kx✝:CharZero KP:K[X]hP:P.Monichca:HasCasasAlveroProp PL:Type u := AlgebraicClosure Kα:Leq:map (algebraMap K L) P = (X - C α) ^ (map (algebraMap K L) P).natDegreeh0:¬P.natDegree = 0α':K := -P.nextCoeff / ↑P.natDegree⊢ (algebraMap K L) (↑P.natDegree)⁻¹ * ↑P.natDegree * α = αnegh:∀ {K : Type u} [inst : Field K] [CharZero K] (P : K[X]),
  P.Monic → HasCasasAlveroPropᵣ P → ∃ α, P = (X - C α) ^ P.natDegreeK:Type ux✝¹:Field Kx✝:CharZero KP:K[X]hP:P.Monichca:HasCasasAlveroProp PL:Type u := AlgebraicClosure Kα:Leq:map (algebraMap K L) P = (X - C α) ^ (map (algebraMap K L) P).natDegreeh0:¬P.natDegree = 0α':K := -P.nextCoeff / ↑P.natDegreethis:(algebraMap K L) α' = α⊢ ∃ α, P = (X - C α) ^ P.natDegree map_inv₀,h:∀ {K : Type u} [inst : Field K] [CharZero K] (P : K[X]),
  P.Monic → HasCasasAlveroPropᵣ P → ∃ α, P = (X - C α) ^ P.natDegreeK:Type ux✝¹:Field Kx✝:CharZero KP:K[X]hP:P.Monichca:HasCasasAlveroProp PL:Type u := AlgebraicClosure Kα:Leq:map (algebraMap K L) P = (X - C α) ^ (map (algebraMap K L) P).natDegreeh0:¬P.natDegree = 0α':K := -P.nextCoeff / ↑P.natDegree⊢ ((algebraMap K L) ↑P.natDegree)⁻¹ * ↑P.natDegree * α = αnegh:∀ {K : Type u} [inst : Field K] [CharZero K] (P : K[X]),
  P.Monic → HasCasasAlveroPropᵣ P → ∃ α, P = (X - C α) ^ P.natDegreeK:Type ux✝¹:Field Kx✝:CharZero KP:K[X]hP:P.Monichca:HasCasasAlveroProp PL:Type u := AlgebraicClosure Kα:Leq:map (algebraMap K L) P = (X - C α) ^ (map (algebraMap K L) P).natDegreeh0:¬P.natDegree = 0α':K := -P.nextCoeff / ↑P.natDegreethis:(algebraMap K L) α' = α⊢ ∃ α, P = (X - C α) ^ P.natDegree map_natCasth:∀ {K : Type u} [inst : Field K] [CharZero K] (P : K[X]),
  P.Monic → HasCasasAlveroPropᵣ P → ∃ α, P = (X - C α) ^ P.natDegreeK:Type ux✝¹:Field Kx✝:CharZero KP:K[X]hP:P.Monichca:HasCasasAlveroProp PL:Type u := AlgebraicClosure Kα:Leq:map (algebraMap K L) P = (X - C α) ^ (map (algebraMap K L) P).natDegreeh0:¬P.natDegree = 0α':K := -P.nextCoeff / ↑P.natDegree⊢ (↑P.natDegree)⁻¹ * ↑P.natDegree * α = αnegh:∀ {K : Type u} [inst : Field K] [CharZero K] (P : K[X]),
  P.Monic → HasCasasAlveroPropᵣ P → ∃ α, P = (X - C α) ^ P.natDegreeK:Type ux✝¹:Field Kx✝:CharZero KP:K[X]hP:P.Monichca:HasCasasAlveroProp PL:Type u := AlgebraicClosure Kα:Leq:map (algebraMap K L) P = (X - C α) ^ (map (algebraMap K L) P).natDegreeh0:¬P.natDegree = 0α':K := -P.nextCoeff / ↑P.natDegreethis:(algebraMap K L) α' = α⊢ ∃ α, P = (X - C α) ^ P.natDegree]
    rw [inv_mul_cancel₀ (Nat.cast_ne_zero.mpr h0),h:∀ {K : Type u} [inst : Field K] [CharZero K] (P : K[X]),
  P.Monic → HasCasasAlveroPropᵣ P → ∃ α, P = (X - C α) ^ P.natDegreeK:Type ux✝¹:Field Kx✝:CharZero KP:K[X]hP:P.Monichca:HasCasasAlveroProp PL:Type u := AlgebraicClosure Kα:Leq:map (algebraMap K L) P = (X - C α) ^ (map (algebraMap K L) P).natDegreeh0:¬P.natDegree = 0α':K := -P.nextCoeff / ↑P.natDegree⊢ 1 * α = αnegh:∀ {K : Type u} [inst : Field K] [CharZero K] (P : K[X]),
  P.Monic → HasCasasAlveroPropᵣ P → ∃ α, P = (X - C α) ^ P.natDegreeK:Type ux✝¹:Field Kx✝:CharZero KP:K[X]hP:P.Monichca:HasCasasAlveroProp PL:Type u := AlgebraicClosure Kα:Leq:map (algebraMap K L) P = (X - C α) ^ (map (algebraMap K L) P).natDegreeh0:¬P.natDegree = 0α':K := -P.nextCoeff / ↑P.natDegreethis:(algebraMap K L) α' = α⊢ ∃ α, P = (X - C α) ^ P.natDegree one_mulh:∀ {K : Type u} [inst : Field K] [CharZero K] (P : K[X]),
  P.Monic → HasCasasAlveroPropᵣ P → ∃ α, P = (X - C α) ^ P.natDegreeK:Type ux✝¹:Field Kx✝:CharZero KP:K[X]hP:P.Monichca:HasCasasAlveroProp PL:Type u := AlgebraicClosure Kα:Leq:map (algebraMap K L) P = (X - C α) ^ (map (algebraMap K L) P).natDegreeh0:¬P.natDegree = 0α':K := -P.nextCoeff / ↑P.natDegree⊢ α = αnegh:∀ {K : Type u} [inst : Field K] [CharZero K] (P : K[X]),
  P.Monic → HasCasasAlveroPropᵣ P → ∃ α, P = (X - C α) ^ P.natDegreeK:Type ux✝¹:Field Kx✝:CharZero KP:K[X]hP:P.Monichca:HasCasasAlveroProp PL:Type u := AlgebraicClosure Kα:Leq:map (algebraMap K L) P = (X - C α) ^ (map (algebraMap K L) P).natDegreeh0:¬P.natDegree = 0α':K := -P.nextCoeff / ↑P.natDegreethis:(algebraMap K L) α' = α⊢ ∃ α, P = (X - C α) ^ P.natDegree]negh:∀ {K : Type u} [inst : Field K] [CharZero K] (P : K[X]),
  P.Monic → HasCasasAlveroPropᵣ P → ∃ α, P = (X - C α) ^ P.natDegreeK:Type ux✝¹:Field Kx✝:CharZero KP:K[X]hP:P.Monichca:HasCasasAlveroProp PL:Type u := AlgebraicClosure Kα:Leq:map (algebraMap K L) P = (X - C α) ^ (map (algebraMap K L) P).natDegreeh0:¬P.natDegree = 0α':K := -P.nextCoeff / ↑P.natDegreethis:(algebraMap K L) α' = α⊢ ∃ α, P = (X - C α) ^ P.natDegreenegh:∀ {K : Type u} [inst : Field K] [CharZero K] (P : K[X]),
  P.Monic → HasCasasAlveroPropᵣ P → ∃ α, P = (X - C α) ^ P.natDegreeK:Type ux✝¹:Field Kx✝:CharZero KP:K[X]hP:P.Monichca:HasCasasAlveroProp PL:Type u := AlgebraicClosure Kα:Leq:map (algebraMap K L) P = (X - C α) ^ (map (algebraMap K L) P).natDegreeh0:¬P.natDegree = 0α':K := -P.nextCoeff / ↑P.natDegreethis:(algebraMap K L) α' = α⊢ ∃ α, P = (X - C α) ^ P.natDegree
  use α'hh:∀ {K : Type u} [inst : Field K] [CharZero K] (P : K[X]),
  P.Monic → HasCasasAlveroPropᵣ P → ∃ α, P = (X - C α) ^ P.natDegreeK:Type ux✝¹:Field Kx✝:CharZero KP:K[X]hP:P.Monichca:HasCasasAlveroProp PL:Type u := AlgebraicClosure Kα:Leq:map (algebraMap K L) P = (X - C α) ^ (map (algebraMap K L) P).natDegreeh0:¬P.natDegree = 0α':K := -P.nextCoeff / ↑P.natDegreethis:(algebraMap K L) α' = α⊢ P = (X - C α') ^ P.natDegree
  apply map_injective _ (algebraMap K L).injectivehh:∀ {K : Type u} [inst : Field K] [CharZero K] (P : K[X]),
  P.Monic → HasCasasAlveroPropᵣ P → ∃ α, P = (X - C α) ^ P.natDegreeK:Type ux✝¹:Field Kx✝:CharZero KP:K[X]hP:P.Monichca:HasCasasAlveroProp PL:Type u := AlgebraicClosure Kα:Leq:map (algebraMap K L) P = (X - C α) ^ (map (algebraMap K L) P).natDegreeh0:¬P.natDegree = 0α':K := -P.nextCoeff / ↑P.natDegreethis:(algebraMap K L) α' = α⊢ map (algebraMap K L) P = map (algebraMap K L) ((X - C α') ^ P.natDegree)
  simpa [this] using eqAll goals completed! 🐙

section conjecturevariable [CharZero K] (P : K[X]) (hP : Monic P)include hP

The Casas-Alvero conjecture states that in characteristic zero, if a monic polynomial P has the Casas-Alvero property, then P = (X - α)ᵈ for some α.

@[category research open, AMS 12]
theorem casas_alvero_conjecture (hP' : HasCasasAlveroProp P) :
    ∃ α : K, P = (X - C α) ^ P.natDegree := byK:Type u_1inst✝¹:Field Kinst✝:CharZero KP:K[X]hP:P.MonichP':HasCasasAlveroProp P⊢ ∃ α, P = (X - C α) ^ P.natDegree
  sorryAll goals completed! 🐙

The Casas-Alvero conjecture holds for polynomials of prime power degree. This was proved by Graf von Bothmer, Labs, Schicho, and van de Woestijne.

Reference: The Casas-Alvero conjecture for infinitely many degrees

@[category research solved, AMS 12]
theorem casas_alvero.prime_power (p k : ℕ) (hp : p.Prime) (hd : P.natDegree = p^k)
    (hP' : HasCasasAlveroProp P) : ∃ α : K, P = (X - C α) ^ P.natDegree := byK:Type u_1inst✝¹:Field Kinst✝:CharZero KP:K[X]hP:P.Monicp:ℕk:ℕhp:Nat.Prime phd:P.natDegree = p ^ khP':HasCasasAlveroProp P⊢ ∃ α, P = (X - C α) ^ P.natDegree
  sorryAll goals completed! 🐙

The Casas-Alvero conjecture holds for polynomials of degree 2p^k where p is prime. This was proved by Graf von Bothmer, Labs, Schicho, and van de Woestijne.

Reference: The Casas-Alvero conjecture for infinitely many degrees

@[category research solved, AMS 12]
theorem casas_alvero.double_prime_power (p k : ℕ) (hp : p.Prime) (hd : P.natDegree = 2 * p^k)
    (hP' : HasCasasAlveroProp P) : ∃ α : K, P = (X - C α) ^ P.natDegree := byK:Type u_1inst✝¹:Field Kinst✝:CharZero KP:K[X]hP:P.Monicp:ℕk:ℕhp:Nat.Prime phd:P.natDegree = 2 * p ^ khP':HasCasasAlveroProp P⊢ ∃ α, P = (X - C α) ^ P.natDegree
  sorryAll goals completed! 🐙

end conjecture

The Casas-Alvero conjecture fails in positive characteristic p for polynomials of degree p + 1. This was shown by Graf von Bothmer, Labs, Schicho, and van de Woestijne.

Reference: The Casas-Alvero conjecture for infinitely many degrees

Formal proof linked here provided by AlphaProof.

@[category research solved, AMS 12, formal_proof using formal_conjectures at "https://github.com/mzhorvath1/formal-conjectures/blob/4f2343508f2c157f35abb7be4814bd550280ce81/FormalConjectures/Paper/CasasAlvero.lean#163"]
theorem casas_alvero.positive_char_counterexample {p : ℕ} (hp : p.Prime) :
    ∃ (K : Type*) (_ : Field K) (_ : CharP K p),
      let P := X ^ (p + 1) - X ^ p
      Monic P ∧ HasCasasAlveroProp P ∧
      ¬∃ α : K, P = (X - C α) ^ P.natDegree := byp:ℕhp:Nat.Prime p⊢ ∃ K x,
  ∃ (_ : CharP K p),
    let P := X ^ (p + 1) - X ^ p;
    P.Monic ∧ HasCasasAlveroProp P ∧ ¬∃ α, P = (X - C α) ^ P.natDegree
  sorryAll goals completed! 🐙

end CasasAlvero