internlm/Lean-Github huggingface dataset:
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' → ℕ)
⊢ IsField R
Tactic:
have h_R: Fintype.card Rˣ = q ^ n - 1 := by
  have : Fintype.card Rˣ + 1 = Fintype.card R := Fintype.card_eq_card_units_add_one.symm
  rw [← h_card, ← this]
  simp only [ge_iff_le, add_le_iff_nonpos_left, nonpos_iff_eq_zero, Fintype.card_ne_zero,
  add_tsub_cancel_right]
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
⊢ IsField R
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
⊢ IsField R
Tactic:
have h_Z : Fintype.card Zˣ = q - 1 := by
  have h : Fintype.card Zˣ + 1 = Fintype.card Z := Fintype.card_eq_card_units_add_one.symm
  have : Fintype.card Z = q := rfl
  rw [← this, ← h]
  simp only [center_toSubsemiring, Subsemiring.center_toSubmonoid, ge_iff_le,
    add_le_iff_nonpos_left, nonpos_iff_eq_zero, Fintype.card_ne_zero, add_tsub_cancel_right]
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
⊢ IsField R
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
⊢ IsField R
Tactic:
have H1:= (Group.card_center_add_sum_card_noncenter_eq_card Rˣ).symm
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 :
  Fintype.card Rˣ =
    Fintype.card ↥(Subgroup.center Rˣ) + ∑ x ∈ (ConjClasses.noncenter Rˣ).toFinset, x.carrier.toFinset.card
⊢ IsField R
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 :
  Fintype.card Rˣ =
    Fintype.card ↥(Subgroup.center Rˣ) + ∑ x ∈ (ConjClasses.noncenter Rˣ).toFinset, x.carrier.toFinset.card
⊢ IsField R
Tactic:
let e := Subgroup.centerUnitsEquivUnitsCenter R
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 :
  Fintype.card Rˣ =
    Fintype.card ↥(Subgroup.center Rˣ) + ∑ x ∈ (ConjClasses.noncenter Rˣ).toFinset, x.carrier.toFinset.card
e : ↥(Subgroup.center Rˣ) ≃* (↥(Submonoid.center R))ˣ := Subgroup.centerUnitsEquivUnitsCenter R
⊢ IsField R
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 :
  Fintype.card Rˣ =
    Fintype.card ↥(Subgroup.center Rˣ) + ∑ x ∈ (ConjClasses.noncenter Rˣ).toFinset, x.carrier.toFinset.card
e : ↥(Subgroup.center Rˣ) ≃* (↥(Submonoid.center R))ˣ := Subgroup.centerUnitsEquivUnitsCenter R
⊢ IsField R
Tactic:
let f : { x // x ∈ Submonoid.center R }ˣ ≃ { x // x ∈ Z }ˣ :=
    Equiv.inv { x // x ∈ Submonoid.center R }ˣ
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 :
  Fintype.card Rˣ =
    Fintype.card ↥(Subgroup.center Rˣ) + ∑ 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))ˣ
⊢ IsField R
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 :
  Fintype.card Rˣ =
    Fintype.card ↥(Subgroup.center Rˣ) + ∑ 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))ˣ
⊢ IsField R
Tactic:
rw [h_R, Fintype.card_congr (e.toEquiv.trans f), h_Z] at H1
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))ˣ
⊢ IsField R
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))ˣ
⊢ IsField R
Tactic:
have : ∀ A : S', (Fintype.card <| ConjClasses.carrier (A : ConjClasses Rˣ)) * (q ^ (n_k A) - 1)
    = q ^ n - 1 := by
  sorry
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
⊢ IsField R
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
⊢ IsField R
Tactic:
have h1 : (q ^ n - 1) = q - 1  + ∑ A : S', (q ^ n - 1) / (q ^ (n_k A) - 1) := by
  convert H1
  sorry
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)
⊢ IsField R
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)
⊢ IsField R
Tactic:
have hZ : Nonempty <| @Subtype R fun x => x ∈ Z := by
    exact Zero.instNonempty
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
⊢ IsField R
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
⊢ IsField R
Tactic:
have hq_pow_pos : ∀ m,  1 ≤ q ^ m := by
  intro m
  refine' one_le_pow m q _
  exact Fintype.card_pos
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
⊢ IsField R