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
g : Polynomial.map (Int.castRingHom ℂ) (phi n) = ∏ lamb ∈ primitiveRoots n ℂ, (X - C lamb)
this✝¹ : 2 ≤ q
h_gt : (eval (↑q) (cyclotomic n ℤ)).natAbs > q - 1
h_q_sub_one : 0 ≠ ↑q - 1
hq_eq : ↑q - 1 = ↑(q - 1)
this✝ : 1 ≤ Fintype.card ↥(center R)
h_q : |↑q - 1| = ↑q - 1
h_norm : |eval (↑q) (phi n)| ≤ ↑(q - 1)
this : ↑(q - 1) = ↑q - 1
⊢ (eval (↑q) (cyclotomic n ℤ)).natAbs ≤ q - 1
Tactic:
have : Int.natAbs (eval (↑q) (cyclotomic n ℤ)) = |eval (↑q) (phi n)| := by
  simp only [Int.natCast_natAbs]
  rfl
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)
this✝² : 2 ≤ q
h_gt : (eval (↑q) (cyclotomic n ℤ)).natAbs > q - 1
h_q_sub_one : 0 ≠ ↑q - 1
hq_eq : ↑q - 1 = ↑(q - 1)
this✝¹ : 1 ≤ Fintype.card ↥(center R)
h_q : |↑q - 1| = ↑q - 1
h_norm : |eval (↑q) (phi n)| ≤ ↑(q - 1)
this✝ : ↑(q - 1) = ↑q - 1
this : ↑(eval (↑q) (cyclotomic n ℤ)).natAbs = |eval (↑q) (phi n)|
⊢ (eval (↑q) (cyclotomic n ℤ)).natAbs ≤ q - 1