internlm/Lean-Github huggingface dataset:
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
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
⊢ 1 < n
Tactic:
sorry
Proof state after:
no goals
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
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
hn : 1 < n
⊢ q ≠ 1
Tactic:
exact Nat.ne_of_gt this
Proof state after:
no goals
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
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
h1 : ↑q - 1 = ↑(q - 1)
⊢ ¬0 = q - 1
Tactic:
exact Nat.ne_of_lt <| Nat.sub_pos_of_lt this
Proof state after:
no goals
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
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
⊢ ↑q - 1 = ↑q - ↑1
Tactic:
norm_num
Proof state after:
no goals
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
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
this : 1 ≤ q
⊢ ↑q - 1 = ↑(q - 1)
Tactic:
simp [this]
Proof state after:
no goals
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
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)
⊢ Nonempty ↥(center R)
Tactic:
exact ⟨1, Subring.one_mem (center R)⟩
Proof state after:
no goals
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
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)
⊢ 1 ≤ q
Tactic:
exact this
Proof state after:
no goals
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
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
⊢ ↑(q - 1) = ↑q - 1
Tactic:
exact Int.natCast_pred_of_pos this
Proof state after:
no goals
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
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 ℤ)| = |eval (↑q) (phi n)|
Tactic:
rfl
Proof state after:
no goals
Theorem: book.quadratic_reciprocity.fermat_little
Proof state before:
p : ℕ
h_p : p ≠ 2
inst✝ : Fact p.Prime
a : ℤ
⊢ ↑a ≠ 0 → ↑a ^ (p - 1) = -1
Tactic:
let units_finset := (Finset.univ : Finset (ZMod p)).erase 0
Proof state after:
p : ℕ
h_p : p ≠ 2
inst✝ : Fact p.Prime
a : ℤ
units_finset : Finset (ZMod p) := univ.erase 0
⊢ ↑a ≠ 0 → ↑a ^ (p - 1) = -1
Theorem: book.quadratic_reciprocity.fermat_little
Proof state before:
p : ℕ
h_p : p ≠ 2
inst✝ : Fact p.Prime
a : ℤ
units_finset : Finset (ZMod p) := univ.erase 0
⊢ ↑a ≠ 0 → ↑a ^ (p - 1) = -1
Tactic:
let image_finset := (units_finset).image (fun x : ZMod p => (a : ZMod p) * x)
Proof state after:
p : ℕ
h_p : p ≠ 2
inst✝ : Fact p.Prime
a : ℤ
units_finset : Finset (ZMod p) := univ.erase 0
image_finset : Finset (ZMod p) := image (fun x => ↑a * x) units_finset
⊢ ↑a ≠ 0 → ↑a ^ (p - 1) = -1
Theorem: book.quadratic_reciprocity.fermat_little
Proof state before:
p : ℕ
h_p : p ≠ 2
inst✝ : Fact p.Prime
a : ℤ
units_finset : Finset (ZMod p) := univ.erase 0
image_finset : Finset (ZMod p) := image (fun x => ↑a * x) units_finset
⊢ ↑a ≠ 0 → ↑a ^ (p - 1) = -1
Tactic:
have : units_finset = image_finset := by sorry
Proof state after:
p : ℕ
h_p : p ≠ 2
inst✝ : Fact p.Prime
a : ℤ
units_finset : Finset (ZMod p) := univ.erase 0
image_finset : Finset (ZMod p) := image (fun x => ↑a * x) units_finset
this : units_finset = image_finset
⊢ ↑a ≠ 0 → ↑a ^ (p - 1) = -1
Theorem: book.quadratic_reciprocity.fermat_little
Proof state before:
p : ℕ
h_p : p ≠ 2
inst✝ : Fact p.Prime
a : ℤ
units_finset : Finset (ZMod p) := univ.erase 0
image_finset : Finset (ZMod p) := image (fun x => ↑a * x) units_finset
this : units_finset = image_finset
⊢ ↑a ≠ 0 → ↑a ^ (p - 1) = -1
Tactic:
sorry
Proof state after:
no goals
Theorem: book.quadratic_reciprocity.fermat_little
Proof state before:
p : ℕ
h_p : p ≠ 2
inst✝ : Fact p.Prime
a : ℤ
units_finset : Finset (ZMod p) := univ.erase 0
image_finset : Finset (ZMod p) := image (fun x => ↑a * x) units_finset
⊢ units_finset = image_finset
Tactic:
sorry
Proof state after:
no goals
Theorem: book.quadratic_reciprocity.euler_criterion
Proof state before:
p : ℕ
h_p : p ≠ 2
inst✝ : Fact p.Prime
a : ℤ
⊢ ↑a ≠ 0 → ↑(legendre_sym p a) = ↑a ^ ((p - 1) / 2)
Tactic:
sorry
Proof state after:
no goals
Theorem: book.quadratic_reciprocity.product_rule
Proof state before:
p : ℕ
h_p : p ≠ 2
inst✝ : Fact p.Prime
a b : ℤ
⊢ legendre_sym p (a * b) = legendre_sym p a * legendre_sym p b
Tactic:
sorry
Proof state after:
no goals
Theorem: book.quadratic_reciprocity.lemma_of_Gauss
Proof state before:
p✝ : ℕ
h_p : p✝ ≠ 2
inst✝¹ : Fact p✝.Prime
p : ℕ
inst✝ : Fact p.Prime
a : ℤ
h_a : ↑a ≠ 0
r : ℤ → ℤ
h_r : ∀ (i : ℤ), (-↑p - 1) / 2 ≤ r i ∧ r i ≤ (↑p - 1) / 2
H : ∀ (i : ℤ), ↑(r i) = ↑a * ↑i
⊢ LocallyFiniteOrder ℤ
Tactic:
sorry
Proof state after:
no goals
Theorem: book.quadratic_reciprocity.lemma_of_Gauss
Proof state before:
p✝ : ℕ
h_p : p✝ ≠ 2
inst✝¹ : Fact p✝.Prime
p : ℕ
inst✝ : Fact p.Prime
a : ℤ
h_a : ↑a ≠ 0
r : ℤ → ℤ
h_r : ∀ (i : ℤ), (-↑p - 1) / 2 ≤ r i ∧ r i ≤ (↑p - 1) / 2
H : ∀ (i : ℤ), ↑(r i) = ↑a * ↑i
⊢ let_fun this := sorryAx (LocallyFiniteOrder ℤ);
  legendre_sym p a = ↑(image r (Icc 1 ((↑p - 1) / 2)) ∩ Icc (-(↑p - 1) / 2) (-1)).card
Tactic:
sorry
Proof state after:
no goals
Theorem: book.quadratic_reciprocity.mult_cyclic
Proof state before:
p : ℕ
h_p : p ≠ 2
inst✝² : Fact p.Prime
K : Type u_1
inst✝¹ : Field K
inst✝ : Fintype K
⊢ ∃ ζ, ∀ (α : Kˣ), ∃ k, α = ζ ^ k
Tactic:
sorry
Proof state after:
no goals
Theorem: book.quadratic_reciprocity.fact_B
Proof state before:
p✝ : ℕ
h_p : p✝ ≠ 2
inst✝² : Fact p✝.Prime
p : ℕ
inst✝¹ : Fact (Prime p)
K : Type u_1
inst✝ : Field K
ζ : Kˣ
h_1 : ζ ^ p = 1
h_2 : ζ ≠ 1
⊢ X ^ (p - 1) - 1 = ∏ i ∈ Icc 1 p, (X - Polynomial.C ↑ζ ^ i)
Tactic:
sorry
Proof state after:
no goals
Theorem: book.quadratic_reciprocity.quadratic_reciprocity_2
Proof state before:
p✝ : ℕ
h_p : p✝ ≠ 2
inst✝² : Fact p✝.Prime
p q : ℕ
hp : p ≠ 2
hq : q ≠ 2
inst✝¹ : Fact p.Prime
inst✝ : Fact q.Prime
⊢ legendre_sym p ↑q * legendre_sym q ↑p = -1 ^ ((p - 1) / 2 * (q - 1) / 2)
Tactic:
sorry
Proof state after:
no goals
Theorem: ramsey_exists
Proof state before:
α : Type ?u.1805
X : Finset α
d : ℕ
h_d : d ≥ 2
m n : ℕ
h_m : m ≥ 2
h_n : n ≥ 2
⊢ ∃ N, ramsey_property m n N
Tactic:
sorry
Proof state after:
no goals
Theorem: Permutation.get_comp
Proof state before:
n : Nat
x y : Permutation n
i : Nat
h : i < n
⊢ (comp x y)[i] = x[↑y[i]]
Tactic:
dsimp [comp]
Proof state after:
n : Nat
x y : Permutation n
i : Nat
h : i < n
⊢ (ofFn (fun i => x[↑y[↑i]]) (_ : ∀ (i j : Fin n), (fun i => x[↑y[↑i]]) i = (fun i => x[↑y[↑i]]) j → i = j))[i] =
    x[↑y[i]]
Theorem: Permutation.get_comp
Proof state before:
n : Nat
x y : Permutation n
i : Nat
h : i < n
⊢ (ofFn (fun i => x[↑y[↑i]]) (_ : ∀ (i j : Fin n), (fun i => x[↑y[↑i]]) i = (fun i => x[↑y[↑i]]) j → i = j))[i] =
    x[↑y[i]]
Tactic:
exact get_ofFn ..
Proof state after:
no goals
Theorem: Permutation.toFun_inv_toFun
Proof state before:
n : Nat
x : Permutation n
i : Fin n
⊢ toFun (inv x) (toFun x i) = i
Tactic:
simp only [inv, toFun_ofFn]
Proof state after:
n : Nat
x : Permutation n
i : Fin n
⊢ Fin.invOfInj (toFun x) (_ : ∀ (i j : Fin n), toFun x i = toFun x j → i = j) (toFun x i) = i
Theorem: Permutation.toFun_inv_toFun
Proof state before:
n : Nat
x : Permutation n
i : Fin n
⊢ Fin.invOfInj (toFun x) (_ : ∀ (i j : Fin n), toFun x i = toFun x j → i = j) (toFun x i) = i
Tactic:
exact Fin.invOfInj_left ..
Proof state after:
no goals
Theorem: Permutation.toFun_toFun_inv
Proof state before:
n : Nat
x : Permutation n
i : Fin n
⊢ toFun x (toFun (inv x) i) = i
Tactic:
simp only [inv, toFun_ofFn]
Proof state after:
n : Nat
x : Permutation n
i : Fin n
⊢ toFun x (Fin.invOfInj (toFun x) (_ : ∀ (i j : Fin n), toFun x i = toFun x j → i = j) i) = i
Theorem: Permutation.toFun_toFun_inv
Proof state before:
n : Nat
x : Permutation n
i : Fin n
⊢ toFun x (Fin.invOfInj (toFun x) (_ : ∀ (i j : Fin n), toFun x i = toFun x j → i = j) i) = i
Tactic:
exact Fin.invOfInj_right ..
Proof state after:
no goals
Theorem: Permutation.get_castAdd_lt
Proof state before:
n m : Nat
x : Permutation n
i : Nat
hi : i < n + m
h : i < n
⊢ (castAdd m x)[i] = Fin.castAdd m x[i]
Tactic:
unfold castAdd GetElem.getElem
Proof state after:
n m : Nat
x : Permutation n
i : Nat
hi : i < n + m
h : i < n
⊢ instGetElemPermutationNatFinLtInstLTNat.1
      { val := Array.map (Fin.castAdd m) x.val ++ Array.ofFn fun i => Fin.cast (_ : m + n = n + m) (Fin.addNat i n),
        size_eq :=
          (_ :
            Array.size
                (Array.map (Fin.castAdd m) x.val ++ Array.ofFn fun i => Fin.cast (_ : m + n = n + m) (Fin.addNat i n)) =
              n + m),
        nodup :=
          (_ :
            Array.Nodup
              (Array.map (Fin.castAdd m) x.val ++ Array.ofFn fun i => Fin.cast (_ : m + n = n + m) (Fin.addNat i n))) }
      i hi =
    Fin.castAdd m (instGetElemPermutationNatFinLtInstLTNat.1 x i h)
Theorem: Permutation.get_castAdd_lt
Proof state before:
n m : Nat
x : Permutation n
i : Nat
hi : i < n + m
h : i < n
⊢ instGetElemPermutationNatFinLtInstLTNat.1
      { val := Array.map (Fin.castAdd m) x.val ++ Array.ofFn fun i => Fin.cast (_ : m + n = n + m) (Fin.addNat i n),
        size_eq :=
          (_ :
            Array.size
                (Array.map (Fin.castAdd m) x.val ++ Array.ofFn fun i => Fin.cast (_ : m + n = n + m) (Fin.addNat i n)) =
              n + m),
        nodup :=
          (_ :
            Array.Nodup
              (Array.map (Fin.castAdd m) x.val ++ Array.ofFn fun i => Fin.cast (_ : m + n = n + m) (Fin.addNat i n))) }
      i hi =
    Fin.castAdd m (instGetElemPermutationNatFinLtInstLTNat.1 x i h)
Tactic:
simp only [instGetElemPermutationNatFinLtInstLTNat]
Proof state after:
n m : Nat
x : Permutation n
i : Nat
hi : i < n + m
h : i < n
⊢ (Array.map (Fin.castAdd m) x.val ++ Array.ofFn fun i => Fin.cast (_ : m + n = n + m) (Fin.addNat i n))[i] =
    Fin.castAdd m x.val[i]
Theorem: Permutation.get_castAdd_lt
Proof state before:
n m : Nat
x : Permutation n
i : Nat
hi : i < n + m
h : i < n
⊢ (Array.map (Fin.castAdd m) x.val ++ Array.ofFn fun i => Fin.cast (_ : m + n = n + m) (Fin.addNat i n))[i] =
    Fin.castAdd m x.val[i]
Tactic:
have : i < x.val.size := x.size_eq.symm ▸ h
Proof state after:
n m : Nat
x : Permutation n
i : Nat
hi : i < n + m
h : i < n
this : i < Array.size x.val
⊢ (Array.map (Fin.castAdd m) x.val ++ Array.ofFn fun i => Fin.cast (_ : m + n = n + m) (Fin.addNat i n))[i] =
    Fin.castAdd m x.val[i]