Theorem: wedderburn
Proof state before:
case intro
R : Type u_1
inst✝¹ : DecidableEq R
inst✝ : DivisionRing R
h : Fintype R
Z : Subring R := center R
n : ℕ
H : ∃ x y, x ≠ y
h_n : n ≠ 0
q : ℕ := Fintype.card ↥Z
h_card : Fintype.card R = q ^ n
finclassa : (A : ConjClasses Rˣ) → Fintype ↑A.carrier
this✝² : (A : ConjClasses Rˣ) → Fintype ↑{Quotient.out' A}.centralizer
fintypea : ConjClasses Rˣ →
  Fintype
    ↑{A |
        let_fun this := finclassa A;
        Fintype.card ↑A.carrier > 1} :=
  fun A =>
    setFintype
      {A |
        let_fun this := finclassa A;
        Fintype.card ↑A.carrier > 1}
this✝¹ :
  Fintype
    ↑{A |
        let_fun this := finclassa A;
        Fintype.card ↑A.carrier > 1}
S' : Set (ConjClasses Rˣ) := ConjClasses.noncenter Rˣ
this✝ : Fintype ↑S'
S : Finset (ConjClasses Rˣ) := S'.toFinset
n_k : ↑S' → ℕ := sorryAx (↑S' → ℕ)
h_R : Fintype.card Rˣ = q ^ n - 1
h_Z : Fintype.card (↥Z)ˣ = q - 1
H1 : q ^ n - 1 = q - 1 + ∑ x ∈ (ConjClasses.noncenter Rˣ).toFinset, x.carrier.toFinset.card
e : ↥(Subgroup.center Rˣ) ≃* (↥(Submonoid.center R))ˣ := Subgroup.centerUnitsEquivUnitsCenter R
f : (↥(Submonoid.center R))ˣ ≃ (↥Z)ˣ := Equiv.inv (↥(Submonoid.center R))ˣ
this : ∀ (A : ↑S'), Fintype.card ↑(↑A).carrier * (q ^ n_k A - 1) = q ^ n - 1
h1 : q ^ n - 1 = q - 1 + ∑ A : ↑S', (q ^ n - 1) / (q ^ n_k A - 1)
hZ : Nonempty ↥Z
hq_pow_pos : ∀ (m : ℕ), 1 ≤ q ^ m
h_n_k_A_dvd : ∀ (A : ↑S'), n_k A ∣ n
h_phi_dvd_q_sub_one : eval (↑q) (phi n) ∣ ↑(q - 1)
x✝ : ¬IsField R
⊢ False
Tactic:
have g : Polynomial.map (Int.castRingHom ℂ) (phi n) = ∏ lamb in (primitiveRoots n ℂ), (X - C lamb) := by
  dsimp only [phi]
  simp only [map_cyclotomic]
  have := isPrimitiveRoot_exp n h_n
  rw [cyclotomic_eq_prod_X_sub_primitiveRoots this]
Proof state after:
case intro
R : Type u_1
inst✝¹ : DecidableEq R
inst✝ : DivisionRing R
h : Fintype R
Z : Subring R := center R
n : ℕ
H : ∃ x y, x ≠ y
h_n : n ≠ 0
q : ℕ := Fintype.card ↥Z
h_card : Fintype.card R = q ^ n
finclassa : (A : ConjClasses Rˣ) → Fintype ↑A.carrier
this✝² : (A : ConjClasses Rˣ) → Fintype ↑{Quotient.out' A}.centralizer
fintypea : ConjClasses Rˣ →
  Fintype
    ↑{A |
        let_fun this := finclassa A;
        Fintype.card ↑A.carrier > 1} :=
  fun A =>
    setFintype
      {A |
        let_fun this := finclassa A;
        Fintype.card ↑A.carrier > 1}
this✝¹ :
  Fintype
    ↑{A |
        let_fun this := finclassa A;
        Fintype.card ↑A.carrier > 1}
S' : Set (ConjClasses Rˣ) := ConjClasses.noncenter Rˣ
this✝ : Fintype ↑S'
S : Finset (ConjClasses Rˣ) := S'.toFinset
n_k : ↑S' → ℕ := sorryAx (↑S' → ℕ)
h_R : Fintype.card Rˣ = q ^ n - 1
h_Z : Fintype.card (↥Z)ˣ = q - 1
H1 : q ^ n - 1 = q - 1 + ∑ x ∈ (ConjClasses.noncenter Rˣ).toFinset, x.carrier.toFinset.card
e : ↥(Subgroup.center Rˣ) ≃* (↥(Submonoid.center R))ˣ := Subgroup.centerUnitsEquivUnitsCenter R
f : (↥(Submonoid.center R))ˣ ≃ (↥Z)ˣ := Equiv.inv (↥(Submonoid.center R))ˣ
this : ∀ (A : ↑S'), Fintype.card ↑(↑A).carrier * (q ^ n_k A - 1) = q ^ n - 1
h1 : q ^ n - 1 = q - 1 + ∑ A : ↑S', (q ^ n - 1) / (q ^ n_k A - 1)
hZ : Nonempty ↥Z
hq_pow_pos : ∀ (m : ℕ), 1 ≤ q ^ m
h_n_k_A_dvd : ∀ (A : ↑S'), n_k A ∣ n
h_phi_dvd_q_sub_one : eval (↑q) (phi n) ∣ ↑(q - 1)
x✝ : ¬IsField R
g : Polynomial.map (Int.castRingHom ℂ) (phi n) = ∏ lamb ∈ primitiveRoots n ℂ, (X - C lamb)
⊢ False