Theorem: wedderburn
Proof state before:
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
hq : q = Fintype.card ↥(center R)
h₁_dvd : eval (↑q) (phi n) ∣ eval (↑q) (X ^ n - 1)
A : ↑S'
hs : A ∈ univ
h_one_neq : 1 ≠ n_k A
h_k_n_lt_n : n_k A < n
⊢ ↑(q ^ n_k A - 1) * eval (↑q) (phi n) ∣ ↑(q ^ n - 1)
Tactic:
have h_noneval := phi_div_2 n (n_k A) h_one_neq (h_n_k_A_dvd A) h_k_n_lt_n
Proof state after:
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
hq : q = Fintype.card ↥(center R)
h₁_dvd : eval (↑q) (phi n) ∣ eval (↑q) (X ^ n - 1)
A : ↑S'
hs : A ∈ univ
h_one_neq : 1 ≠ n_k A
h_k_n_lt_n : n_k A < n
h_noneval : (X ^ n_k A - 1) * phi n ∣ X ^ n - 1
⊢ ↑(q ^ n_k A - 1) * eval (↑q) (phi n) ∣ ↑(q ^ n - 1)