internlm/Lean-Github huggingface dataset:
Theorem: false_of_zeta_sub_one_pow_dvd_sub_one_of_pow_ne
Proof state before:
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝⁷ : Field K
inst✝⁶ : NumberField K
inst✝⁵ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
inst✝⁴ : Fintype (ClassGroup (𝓞 K))
hreg : (↑p).Coprime (Fintype.card (ClassGroup (𝓞 K)))
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
u✝ : (𝓞 K)ˣ
hcong✝ : (↑hζ.unit' - 1) ^ ↑p ∣ ↑u✝ - 1
hu✝ : ∀ (v : K), v ^ ↑p ≠ (algebraMap (𝓞 K) K) ↑u✝
L✝ : Type ?u.27748
inst✝³ : Field L✝
inst✝² : Algebra K L✝
inst✝¹ : FiniteDimensional K L✝
inst✝ : IsSplittingField K L✝ (X ^ ↑p - C ((algebraMap (𝓞 K) K) ↑u✝))
σ : L✝ ≃ₐ[K] L✝
hσ : ∀ (x : L✝ ≃ₐ[K] L✝), x ∈ Subgroup.zpowers σ
u : (𝓞 K)ˣ
hcong : (↑hζ.unit' - 1) ^ ↑p ∣ ↑u - 1
hu : ∀ (v : K), v ^ ↑p ≠ (algebraMap (𝓞 K) K) ↑u
this✝⁴ : Fact (Irreducible (X ^ ↑p - C ((algebraMap (𝓞 K) K) ↑u))) :=
  { out := X_pow_sub_C_irreducible_of_prime Fact.out hu }
L : Type u_1 := AdjoinRoot (X ^ ↑p - C ((algebraMap (𝓞 K) K) ↑u))
this✝³ : IsSplittingField K (AdjoinRoot (X ^ ↑p - C ((algebraMap (𝓞 K) K) ↑u))) (X ^ ↑p - C ((algebraMap (𝓞 K) K) ↑u))
this✝² : IsGalois K L
this✝¹ : FiniteDimensional K L
this✝ : IsCyclic (L ≃ₐ[K] L)
this : CharZero L
⊢ False
Tactic:
have : FiniteDimensional ℚ L := Module.Finite.trans K L
Proof state after:
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝⁷ : Field K
inst✝⁶ : NumberField K
inst✝⁵ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
inst✝⁴ : Fintype (ClassGroup (𝓞 K))
hreg : (↑p).Coprime (Fintype.card (ClassGroup (𝓞 K)))
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
u✝ : (𝓞 K)ˣ
hcong✝ : (↑hζ.unit' - 1) ^ ↑p ∣ ↑u✝ - 1
hu✝ : ∀ (v : K), v ^ ↑p ≠ (algebraMap (𝓞 K) K) ↑u✝
L✝ : Type ?u.27748
inst✝³ : Field L✝
inst✝² : Algebra K L✝
inst✝¹ : FiniteDimensional K L✝
inst✝ : IsSplittingField K L✝ (X ^ ↑p - C ((algebraMap (𝓞 K) K) ↑u✝))
σ : L✝ ≃ₐ[K] L✝
hσ : ∀ (x : L✝ ≃ₐ[K] L✝), x ∈ Subgroup.zpowers σ
u : (𝓞 K)ˣ
hcong : (↑hζ.unit' - 1) ^ ↑p ∣ ↑u - 1
hu : ∀ (v : K), v ^ ↑p ≠ (algebraMap (𝓞 K) K) ↑u
this✝⁵ : Fact (Irreducible (X ^ ↑p - C ((algebraMap (𝓞 K) K) ↑u))) :=
  { out := X_pow_sub_C_irreducible_of_prime Fact.out hu }
L : Type u_1 := AdjoinRoot (X ^ ↑p - C ((algebraMap (𝓞 K) K) ↑u))
this✝⁴ : IsSplittingField K (AdjoinRoot (X ^ ↑p - C ((algebraMap (𝓞 K) K) ↑u))) (X ^ ↑p - C ((algebraMap (𝓞 K) K) ↑u))
this✝³ : IsGalois K L
this✝² : FiniteDimensional K L
this✝¹ : IsCyclic (L ≃ₐ[K] L)
this✝ : CharZero L
this : FiniteDimensional ℚ L
⊢ False
Theorem: false_of_zeta_sub_one_pow_dvd_sub_one_of_pow_ne
Proof state before:
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝⁷ : Field K
inst✝⁶ : NumberField K
inst✝⁵ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
inst✝⁴ : Fintype (ClassGroup (𝓞 K))
hreg : (↑p).Coprime (Fintype.card (ClassGroup (𝓞 K)))
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
u✝ : (𝓞 K)ˣ
hcong✝ : (↑hζ.unit' - 1) ^ ↑p ∣ ↑u✝ - 1
hu✝ : ∀ (v : K), v ^ ↑p ≠ (algebraMap (𝓞 K) K) ↑u✝
L✝ : Type ?u.27748
inst✝³ : Field L✝
inst✝² : Algebra K L✝
inst✝¹ : FiniteDimensional K L✝
inst✝ : IsSplittingField K L✝ (X ^ ↑p - C ((algebraMap (𝓞 K) K) ↑u✝))
σ : L✝ ≃ₐ[K] L✝
hσ : ∀ (x : L✝ ≃ₐ[K] L✝), x ∈ Subgroup.zpowers σ
u : (𝓞 K)ˣ
hcong : (↑hζ.unit' - 1) ^ ↑p ∣ ↑u - 1
hu : ∀ (v : K), v ^ ↑p ≠ (algebraMap (𝓞 K) K) ↑u
this✝⁵ : Fact (Irreducible (X ^ ↑p - C ((algebraMap (𝓞 K) K) ↑u))) :=
  { out := X_pow_sub_C_irreducible_of_prime Fact.out hu }
L : Type u_1 := AdjoinRoot (X ^ ↑p - C ((algebraMap (𝓞 K) K) ↑u))
this✝⁴ : IsSplittingField K (AdjoinRoot (X ^ ↑p - C ((algebraMap (𝓞 K) K) ↑u))) (X ^ ↑p - C ((algebraMap (𝓞 K) K) ↑u))
this✝³ : IsGalois K L
this✝² : FiniteDimensional K L
this✝¹ : IsCyclic (L ≃ₐ[K] L)
this✝ : CharZero L
this : FiniteDimensional ℚ L
⊢ False
Tactic:
have : NumberField L := ⟨⟩
Proof state after:
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝⁷ : Field K
inst✝⁶ : NumberField K
inst✝⁵ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
inst✝⁴ : Fintype (ClassGroup (𝓞 K))
hreg : (↑p).Coprime (Fintype.card (ClassGroup (𝓞 K)))
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
u✝ : (𝓞 K)ˣ
hcong✝ : (↑hζ.unit' - 1) ^ ↑p ∣ ↑u✝ - 1
hu✝ : ∀ (v : K), v ^ ↑p ≠ (algebraMap (𝓞 K) K) ↑u✝
L✝ : Type ?u.27748
inst✝³ : Field L✝
inst✝² : Algebra K L✝
inst✝¹ : FiniteDimensional K L✝
inst✝ : IsSplittingField K L✝ (X ^ ↑p - C ((algebraMap (𝓞 K) K) ↑u✝))
σ : L✝ ≃ₐ[K] L✝
hσ : ∀ (x : L✝ ≃ₐ[K] L✝), x ∈ Subgroup.zpowers σ
u : (𝓞 K)ˣ
hcong : (↑hζ.unit' - 1) ^ ↑p ∣ ↑u - 1
hu : ∀ (v : K), v ^ ↑p ≠ (algebraMap (𝓞 K) K) ↑u
this✝⁶ : Fact (Irreducible (X ^ ↑p - C ((algebraMap (𝓞 K) K) ↑u))) :=
  { out := X_pow_sub_C_irreducible_of_prime Fact.out hu }
L : Type u_1 := AdjoinRoot (X ^ ↑p - C ((algebraMap (𝓞 K) K) ↑u))
this✝⁵ : IsSplittingField K (AdjoinRoot (X ^ ↑p - C ((algebraMap (𝓞 K) K) ↑u))) (X ^ ↑p - C ((algebraMap (𝓞 K) K) ↑u))
this✝⁴ : IsGalois K L
this✝³ : FiniteDimensional K L
this✝² : IsCyclic (L ≃ₐ[K] L)
this✝¹ : CharZero L
this✝ : FiniteDimensional ℚ L
this : NumberField L
⊢ False
Theorem: false_of_zeta_sub_one_pow_dvd_sub_one_of_pow_ne
Proof state before:
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝⁷ : Field K
inst✝⁶ : NumberField K
inst✝⁵ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
inst✝⁴ : Fintype (ClassGroup (𝓞 K))
hreg : (↑p).Coprime (Fintype.card (ClassGroup (𝓞 K)))
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
u✝ : (𝓞 K)ˣ
hcong✝ : (↑hζ.unit' - 1) ^ ↑p ∣ ↑u✝ - 1
hu✝ : ∀ (v : K), v ^ ↑p ≠ (algebraMap (𝓞 K) K) ↑u✝
L✝ : Type ?u.27748
inst✝³ : Field L✝
inst✝² : Algebra K L✝
inst✝¹ : FiniteDimensional K L✝
inst✝ : IsSplittingField K L✝ (X ^ ↑p - C ((algebraMap (𝓞 K) K) ↑u✝))
σ : L✝ ≃ₐ[K] L✝
hσ : ∀ (x : L✝ ≃ₐ[K] L✝), x ∈ Subgroup.zpowers σ
u : (𝓞 K)ˣ
hcong : (↑hζ.unit' - 1) ^ ↑p ∣ ↑u - 1
hu : ∀ (v : K), v ^ ↑p ≠ (algebraMap (𝓞 K) K) ↑u
this✝⁶ : Fact (Irreducible (X ^ ↑p - C ((algebraMap (𝓞 K) K) ↑u))) :=
  { out := X_pow_sub_C_irreducible_of_prime Fact.out hu }
L : Type u_1 := AdjoinRoot (X ^ ↑p - C ((algebraMap (𝓞 K) K) ↑u))
this✝⁵ : IsSplittingField K (AdjoinRoot (X ^ ↑p - C ((algebraMap (𝓞 K) K) ↑u))) (X ^ ↑p - C ((algebraMap (𝓞 K) K) ↑u))
this✝⁴ : IsGalois K L
this✝³ : FiniteDimensional K L
this✝² : IsCyclic (L ≃ₐ[K] L)
this✝¹ : CharZero L
this✝ : FiniteDimensional ℚ L
this : NumberField L
⊢ False
Tactic:
have hKL : FiniteDimensional.finrank K L = p := (finrank_of_isSplittingField_X_pow_sub_C
  ⟨ζ, (mem_primitiveRoots p.pos).mpr hζ⟩ (X_pow_sub_C_irreducible_of_prime hpri.out hu) L)
Proof state after:
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝⁷ : Field K
inst✝⁶ : NumberField K
inst✝⁵ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
inst✝⁴ : Fintype (ClassGroup (𝓞 K))
hreg : (↑p).Coprime (Fintype.card (ClassGroup (𝓞 K)))
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
u✝ : (𝓞 K)ˣ
hcong✝ : (↑hζ.unit' - 1) ^ ↑p ∣ ↑u✝ - 1
hu✝ : ∀ (v : K), v ^ ↑p ≠ (algebraMap (𝓞 K) K) ↑u✝
L✝ : Type ?u.27748
inst✝³ : Field L✝
inst✝² : Algebra K L✝
inst✝¹ : FiniteDimensional K L✝
inst✝ : IsSplittingField K L✝ (X ^ ↑p - C ((algebraMap (𝓞 K) K) ↑u✝))
σ : L✝ ≃ₐ[K] L✝
hσ : ∀ (x : L✝ ≃ₐ[K] L✝), x ∈ Subgroup.zpowers σ
u : (𝓞 K)ˣ
hcong : (↑hζ.unit' - 1) ^ ↑p ∣ ↑u - 1
hu : ∀ (v : K), v ^ ↑p ≠ (algebraMap (𝓞 K) K) ↑u
this✝⁶ : Fact (Irreducible (X ^ ↑p - C ((algebraMap (𝓞 K) K) ↑u))) :=
  { out := X_pow_sub_C_irreducible_of_prime Fact.out hu }
L : Type u_1 := AdjoinRoot (X ^ ↑p - C ((algebraMap (𝓞 K) K) ↑u))
this✝⁵ : IsSplittingField K (AdjoinRoot (X ^ ↑p - C ((algebraMap (𝓞 K) K) ↑u))) (X ^ ↑p - C ((algebraMap (𝓞 K) K) ↑u))
this✝⁴ : IsGalois K L
this✝³ : FiniteDimensional K L
this✝² : IsCyclic (L ≃ₐ[K] L)
this✝¹ : CharZero L
this✝ : FiniteDimensional ℚ L
this : NumberField L
hKL : FiniteDimensional.finrank K L = ↑p
⊢ False
Theorem: false_of_zeta_sub_one_pow_dvd_sub_one_of_pow_ne
Proof state before:
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝⁷ : Field K
inst✝⁶ : NumberField K
inst✝⁵ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
inst✝⁴ : Fintype (ClassGroup (𝓞 K))
hreg : (↑p).Coprime (Fintype.card (ClassGroup (𝓞 K)))
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
u✝ : (𝓞 K)ˣ
hcong✝ : (↑hζ.unit' - 1) ^ ↑p ∣ ↑u✝ - 1
hu✝ : ∀ (v : K), v ^ ↑p ≠ (algebraMap (𝓞 K) K) ↑u✝
L✝ : Type ?u.27748
inst✝³ : Field L✝
inst✝² : Algebra K L✝
inst✝¹ : FiniteDimensional K L✝
inst✝ : IsSplittingField K L✝ (X ^ ↑p - C ((algebraMap (𝓞 K) K) ↑u✝))
σ : L✝ ≃ₐ[K] L✝
hσ : ∀ (x : L✝ ≃ₐ[K] L✝), x ∈ Subgroup.zpowers σ
u : (𝓞 K)ˣ
hcong : (↑hζ.unit' - 1) ^ ↑p ∣ ↑u - 1
hu : ∀ (v : K), v ^ ↑p ≠ (algebraMap (𝓞 K) K) ↑u
this✝⁶ : Fact (Irreducible (X ^ ↑p - C ((algebraMap (𝓞 K) K) ↑u))) :=
  { out := X_pow_sub_C_irreducible_of_prime Fact.out hu }
L : Type u_1 := AdjoinRoot (X ^ ↑p - C ((algebraMap (𝓞 K) K) ↑u))
this✝⁵ : IsSplittingField K (AdjoinRoot (X ^ ↑p - C ((algebraMap (𝓞 K) K) ↑u))) (X ^ ↑p - C ((algebraMap (𝓞 K) K) ↑u))
this✝⁴ : IsGalois K L
this✝³ : FiniteDimensional K L
this✝² : IsCyclic (L ≃ₐ[K] L)
this✝¹ : CharZero L
this✝ : FiniteDimensional ℚ L
this : NumberField L
hKL : FiniteDimensional.finrank K L = ↑p
⊢ False
Tactic:
have := KummersLemma.isUnramified hp hζ u hcong hu L
Proof state after:
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝⁷ : Field K
inst✝⁶ : NumberField K
inst✝⁵ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
inst✝⁴ : Fintype (ClassGroup (𝓞 K))
hreg : (↑p).Coprime (Fintype.card (ClassGroup (𝓞 K)))
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
u✝ : (𝓞 K)ˣ
hcong✝ : (↑hζ.unit' - 1) ^ ↑p ∣ ↑u✝ - 1
hu✝ : ∀ (v : K), v ^ ↑p ≠ (algebraMap (𝓞 K) K) ↑u✝
L✝ : Type ?u.27748
inst✝³ : Field L✝
inst✝² : Algebra K L✝
inst✝¹ : FiniteDimensional K L✝
inst✝ : IsSplittingField K L✝ (X ^ ↑p - C ((algebraMap (𝓞 K) K) ↑u✝))
σ : L✝ ≃ₐ[K] L✝
hσ : ∀ (x : L✝ ≃ₐ[K] L✝), x ∈ Subgroup.zpowers σ
u : (𝓞 K)ˣ
hcong : (↑hζ.unit' - 1) ^ ↑p ∣ ↑u - 1
hu : ∀ (v : K), v ^ ↑p ≠ (algebraMap (𝓞 K) K) ↑u
this✝⁷ : Fact (Irreducible (X ^ ↑p - C ((algebraMap (𝓞 K) K) ↑u))) :=
  { out := X_pow_sub_C_irreducible_of_prime Fact.out hu }
L : Type u_1 := AdjoinRoot (X ^ ↑p - C ((algebraMap (𝓞 K) K) ↑u))
this✝⁶ : IsSplittingField K (AdjoinRoot (X ^ ↑p - C ((algebraMap (𝓞 K) K) ↑u))) (X ^ ↑p - C ((algebraMap (𝓞 K) K) ↑u))
this✝⁵ : IsGalois K L
this✝⁴ : FiniteDimensional K L
this✝³ : IsCyclic (L ≃ₐ[K] L)
this✝² : CharZero L
this✝¹ : FiniteDimensional ℚ L
this✝ : NumberField L
hKL : FiniteDimensional.finrank K L = ↑p
this : IsUnramified (𝓞 K) (𝓞 L)
⊢ False
Theorem: false_of_zeta_sub_one_pow_dvd_sub_one_of_pow_ne
Proof state before:
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝⁷ : Field K
inst✝⁶ : NumberField K
inst✝⁵ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
inst✝⁴ : Fintype (ClassGroup (𝓞 K))
hreg : (↑p).Coprime (Fintype.card (ClassGroup (𝓞 K)))
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
u✝ : (𝓞 K)ˣ
hcong✝ : (↑hζ.unit' - 1) ^ ↑p ∣ ↑u✝ - 1
hu✝ : ∀ (v : K), v ^ ↑p ≠ (algebraMap (𝓞 K) K) ↑u✝
L✝ : Type ?u.27748
inst✝³ : Field L✝
inst✝² : Algebra K L✝
inst✝¹ : FiniteDimensional K L✝
inst✝ : IsSplittingField K L✝ (X ^ ↑p - C ((algebraMap (𝓞 K) K) ↑u✝))
σ : L✝ ≃ₐ[K] L✝
hσ : ∀ (x : L✝ ≃ₐ[K] L✝), x ∈ Subgroup.zpowers σ
u : (𝓞 K)ˣ
hcong : (↑hζ.unit' - 1) ^ ↑p ∣ ↑u - 1
hu : ∀ (v : K), v ^ ↑p ≠ (algebraMap (𝓞 K) K) ↑u
this✝⁷ : Fact (Irreducible (X ^ ↑p - C ((algebraMap (𝓞 K) K) ↑u))) :=
  { out := X_pow_sub_C_irreducible_of_prime Fact.out hu }
L : Type u_1 := AdjoinRoot (X ^ ↑p - C ((algebraMap (𝓞 K) K) ↑u))
this✝⁶ : IsSplittingField K (AdjoinRoot (X ^ ↑p - C ((algebraMap (𝓞 K) K) ↑u))) (X ^ ↑p - C ((algebraMap (𝓞 K) K) ↑u))
this✝⁵ : IsGalois K L
this✝⁴ : FiniteDimensional K L
this✝³ : IsCyclic (L ≃ₐ[K] L)
this✝² : CharZero L
this✝¹ : FiniteDimensional ℚ L
this✝ : NumberField L
hKL : FiniteDimensional.finrank K L = ↑p
this : IsUnramified (𝓞 K) (𝓞 L)
⊢ False
Tactic:
have := dvd_card_classGroup_of_isUnramified_isCyclic K L (hKL.symm ▸ hpri.out)
  (hKL.symm ▸ PNat.coe_injective.ne hp)
Proof state after:
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝⁷ : Field K
inst✝⁶ : NumberField K
inst✝⁵ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
inst✝⁴ : Fintype (ClassGroup (𝓞 K))
hreg : (↑p).Coprime (Fintype.card (ClassGroup (𝓞 K)))
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
u✝ : (𝓞 K)ˣ
hcong✝ : (↑hζ.unit' - 1) ^ ↑p ∣ ↑u✝ - 1
hu✝ : ∀ (v : K), v ^ ↑p ≠ (algebraMap (𝓞 K) K) ↑u✝
L✝ : Type ?u.27748
inst✝³ : Field L✝
inst✝² : Algebra K L✝
inst✝¹ : FiniteDimensional K L✝
inst✝ : IsSplittingField K L✝ (X ^ ↑p - C ((algebraMap (𝓞 K) K) ↑u✝))
σ : L✝ ≃ₐ[K] L✝
hσ : ∀ (x : L✝ ≃ₐ[K] L✝), x ∈ Subgroup.zpowers σ
u : (𝓞 K)ˣ
hcong : (↑hζ.unit' - 1) ^ ↑p ∣ ↑u - 1
hu : ∀ (v : K), v ^ ↑p ≠ (algebraMap (𝓞 K) K) ↑u
this✝⁸ : Fact (Irreducible (X ^ ↑p - C ((algebraMap (𝓞 K) K) ↑u))) :=
  { out := X_pow_sub_C_irreducible_of_prime Fact.out hu }
L : Type u_1 := AdjoinRoot (X ^ ↑p - C ((algebraMap (𝓞 K) K) ↑u))
this✝⁷ : IsSplittingField K (AdjoinRoot (X ^ ↑p - C ((algebraMap (𝓞 K) K) ↑u))) (X ^ ↑p - C ((algebraMap (𝓞 K) K) ↑u))
this✝⁶ : IsGalois K L
this✝⁵ : FiniteDimensional K L
this✝⁴ : IsCyclic (L ≃ₐ[K] L)
this✝³ : CharZero L
this✝² : FiniteDimensional ℚ L
this✝¹ : NumberField L
hKL : FiniteDimensional.finrank K L = ↑p
this✝ : IsUnramified (𝓞 K) (𝓞 L)
this : FiniteDimensional.finrank K L ∣ Fintype.card (ClassGroup (𝓞 K))
⊢ False
Theorem: false_of_zeta_sub_one_pow_dvd_sub_one_of_pow_ne
Proof state before:
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝⁷ : Field K
inst✝⁶ : NumberField K
inst✝⁵ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
inst✝⁴ : Fintype (ClassGroup (𝓞 K))
hreg : (↑p).Coprime (Fintype.card (ClassGroup (𝓞 K)))
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
u✝ : (𝓞 K)ˣ
hcong✝ : (↑hζ.unit' - 1) ^ ↑p ∣ ↑u✝ - 1
hu✝ : ∀ (v : K), v ^ ↑p ≠ (algebraMap (𝓞 K) K) ↑u✝
L✝ : Type ?u.27748
inst✝³ : Field L✝
inst✝² : Algebra K L✝
inst✝¹ : FiniteDimensional K L✝
inst✝ : IsSplittingField K L✝ (X ^ ↑p - C ((algebraMap (𝓞 K) K) ↑u✝))
σ : L✝ ≃ₐ[K] L✝
hσ : ∀ (x : L✝ ≃ₐ[K] L✝), x ∈ Subgroup.zpowers σ
u : (𝓞 K)ˣ
hcong : (↑hζ.unit' - 1) ^ ↑p ∣ ↑u - 1
hu : ∀ (v : K), v ^ ↑p ≠ (algebraMap (𝓞 K) K) ↑u
this✝⁸ : Fact (Irreducible (X ^ ↑p - C ((algebraMap (𝓞 K) K) ↑u))) :=
  { out := X_pow_sub_C_irreducible_of_prime Fact.out hu }
L : Type u_1 := AdjoinRoot (X ^ ↑p - C ((algebraMap (𝓞 K) K) ↑u))
this✝⁷ : IsSplittingField K (AdjoinRoot (X ^ ↑p - C ((algebraMap (𝓞 K) K) ↑u))) (X ^ ↑p - C ((algebraMap (𝓞 K) K) ↑u))
this✝⁶ : IsGalois K L
this✝⁵ : FiniteDimensional K L
this✝⁴ : IsCyclic (L ≃ₐ[K] L)
this✝³ : CharZero L
this✝² : FiniteDimensional ℚ L
this✝¹ : NumberField L
hKL : FiniteDimensional.finrank K L = ↑p
this✝ : IsUnramified (𝓞 K) (𝓞 L)
this : FiniteDimensional.finrank K L ∣ Fintype.card (ClassGroup (𝓞 K))
⊢ False
Tactic:
rw [hKL, ← Int.ofNat_dvd, (Nat.prime_iff_prime_int.mp hpri.out).irreducible.dvd_iff_not_coprime,
  Nat.isCoprime_iff_coprime] at this
Proof state after:
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝⁷ : Field K
inst✝⁶ : NumberField K
inst✝⁵ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
inst✝⁴ : Fintype (ClassGroup (𝓞 K))
hreg : (↑p).Coprime (Fintype.card (ClassGroup (𝓞 K)))
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
u✝ : (𝓞 K)ˣ
hcong✝ : (↑hζ.unit' - 1) ^ ↑p ∣ ↑u✝ - 1
hu✝ : ∀ (v : K), v ^ ↑p ≠ (algebraMap (𝓞 K) K) ↑u✝
L✝ : Type ?u.27748
inst✝³ : Field L✝
inst✝² : Algebra K L✝
inst✝¹ : FiniteDimensional K L✝
inst✝ : IsSplittingField K L✝ (X ^ ↑p - C ((algebraMap (𝓞 K) K) ↑u✝))
σ : L✝ ≃ₐ[K] L✝
hσ : ∀ (x : L✝ ≃ₐ[K] L✝), x ∈ Subgroup.zpowers σ
u : (𝓞 K)ˣ
hcong : (↑hζ.unit' - 1) ^ ↑p ∣ ↑u - 1
hu : ∀ (v : K), v ^ ↑p ≠ (algebraMap (𝓞 K) K) ↑u
this✝⁸ : Fact (Irreducible (X ^ ↑p - C ((algebraMap (𝓞 K) K) ↑u))) :=
  { out := X_pow_sub_C_irreducible_of_prime Fact.out hu }
L : Type u_1 := AdjoinRoot (X ^ ↑p - C ((algebraMap (𝓞 K) K) ↑u))
this✝⁷ : IsSplittingField K (AdjoinRoot (X ^ ↑p - C ((algebraMap (𝓞 K) K) ↑u))) (X ^ ↑p - C ((algebraMap (𝓞 K) K) ↑u))
this✝⁶ : IsGalois K L
this✝⁵ : FiniteDimensional K L
this✝⁴ : IsCyclic (L ≃ₐ[K] L)
this✝³ : CharZero L
this✝² : FiniteDimensional ℚ L
this✝¹ : NumberField L
hKL : FiniteDimensional.finrank K L = ↑p
this✝ : IsUnramified (𝓞 K) (𝓞 L)
this : ¬(↑p).Coprime (Fintype.card (ClassGroup (𝓞 K)))
⊢ False
Theorem: false_of_zeta_sub_one_pow_dvd_sub_one_of_pow_ne
Proof state before:
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝⁷ : Field K
inst✝⁶ : NumberField K
inst✝⁵ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
inst✝⁴ : Fintype (ClassGroup (𝓞 K))
hreg : (↑p).Coprime (Fintype.card (ClassGroup (𝓞 K)))
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
u✝ : (𝓞 K)ˣ
hcong✝ : (↑hζ.unit' - 1) ^ ↑p ∣ ↑u✝ - 1
hu✝ : ∀ (v : K), v ^ ↑p ≠ (algebraMap (𝓞 K) K) ↑u✝
L✝ : Type ?u.27748
inst✝³ : Field L✝
inst✝² : Algebra K L✝
inst✝¹ : FiniteDimensional K L✝
inst✝ : IsSplittingField K L✝ (X ^ ↑p - C ((algebraMap (𝓞 K) K) ↑u✝))
σ : L✝ ≃ₐ[K] L✝
hσ : ∀ (x : L✝ ≃ₐ[K] L✝), x ∈ Subgroup.zpowers σ
u : (𝓞 K)ˣ
hcong : (↑hζ.unit' - 1) ^ ↑p ∣ ↑u - 1
hu : ∀ (v : K), v ^ ↑p ≠ (algebraMap (𝓞 K) K) ↑u
this✝⁸ : Fact (Irreducible (X ^ ↑p - C ((algebraMap (𝓞 K) K) ↑u))) :=
  { out := X_pow_sub_C_irreducible_of_prime Fact.out hu }
L : Type u_1 := AdjoinRoot (X ^ ↑p - C ((algebraMap (𝓞 K) K) ↑u))
this✝⁷ : IsSplittingField K (AdjoinRoot (X ^ ↑p - C ((algebraMap (𝓞 K) K) ↑u))) (X ^ ↑p - C ((algebraMap (𝓞 K) K) ↑u))
this✝⁶ : IsGalois K L
this✝⁵ : FiniteDimensional K L
this✝⁴ : IsCyclic (L ≃ₐ[K] L)
this✝³ : CharZero L
this✝² : FiniteDimensional ℚ L
this✝¹ : NumberField L
hKL : FiniteDimensional.finrank K L = ↑p
this✝ : IsUnramified (𝓞 K) (𝓞 L)
this : ¬(↑p).Coprime (Fintype.card (ClassGroup (𝓞 K)))
⊢ False
Tactic:
exact this (by convert hreg)
Proof state after:
no goals
Theorem: false_of_zeta_sub_one_pow_dvd_sub_one_of_pow_ne
Proof state before:
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝⁷ : Field K
inst✝⁶ : NumberField K
inst✝⁵ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
inst✝⁴ : Fintype (ClassGroup (𝓞 K))
hreg : (↑p).Coprime (Fintype.card (ClassGroup (𝓞 K)))
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
u✝ : (𝓞 K)ˣ
hcong✝ : (↑hζ.unit' - 1) ^ ↑p ∣ ↑u✝ - 1
hu✝ : ∀ (v : K), v ^ ↑p ≠ (algebraMap (𝓞 K) K) ↑u✝
L✝ : Type ?u.27748
inst✝³ : Field L✝
inst✝² : Algebra K L✝
inst✝¹ : FiniteDimensional K L✝
inst✝ : IsSplittingField K L✝ (X ^ ↑p - C ((algebraMap (𝓞 K) K) ↑u✝))
σ : L✝ ≃ₐ[K] L✝
hσ : ∀ (x : L✝ ≃ₐ[K] L✝), x ∈ Subgroup.zpowers σ
u : (𝓞 K)ˣ
hcong : (↑hζ.unit' - 1) ^ ↑p ∣ ↑u - 1
hu : ∀ (v : K), v ^ ↑p ≠ (algebraMap (𝓞 K) K) ↑u
this✝⁸ : Fact (Irreducible (X ^ ↑p - C ((algebraMap (𝓞 K) K) ↑u))) :=
  { out := X_pow_sub_C_irreducible_of_prime Fact.out hu }
L : Type u_1 := AdjoinRoot (X ^ ↑p - C ((algebraMap (𝓞 K) K) ↑u))
this✝⁷ : IsSplittingField K (AdjoinRoot (X ^ ↑p - C ((algebraMap (𝓞 K) K) ↑u))) (X ^ ↑p - C ((algebraMap (𝓞 K) K) ↑u))
this✝⁶ : IsGalois K L
this✝⁵ : FiniteDimensional K L
this✝⁴ : IsCyclic (L ≃ₐ[K] L)
this✝³ : CharZero L
this✝² : FiniteDimensional ℚ L
this✝¹ : NumberField L
hKL : FiniteDimensional.finrank K L = ↑p
this✝ : IsUnramified (𝓞 K) (𝓞 L)
this : ¬(↑p).Coprime (Fintype.card (ClassGroup (𝓞 K)))
⊢ (↑p).Coprime (Fintype.card (ClassGroup (𝓞 K)))
Tactic:
convert hreg
Proof state after:
no goals
Theorem: eq_pow_prime_of_unit_of_congruent
Proof state before:
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝⁷ : Field K
inst✝⁶ : NumberField K
inst✝⁵ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
inst✝⁴ : Fintype (ClassGroup (𝓞 K))
hreg : (↑p).Coprime (Fintype.card (ClassGroup (𝓞 K)))
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
u✝ : (𝓞 K)ˣ
hcong✝ : (↑hζ.unit' - 1) ^ ↑p ∣ ↑u✝ - 1
hu : ∀ (v : K), v ^ ↑p ≠ (algebraMap (𝓞 K) K) ↑u✝
L : Type ?u.56521
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : FiniteDimensional K L
inst✝ : IsSplittingField K L (X ^ ↑p - C ((algebraMap (𝓞 K) K) ↑u✝))
σ : L ≃ₐ[K] L
hσ : ∀ (x : L ≃ₐ[K] L), x ∈ Subgroup.zpowers σ
u : (𝓞 K)ˣ
hcong : ∃ n, ↑↑p ∣ ↑u - ↑n
⊢ ∃ v, u = v ^ ↑p
Tactic:
haveI : Fact (Nat.Prime p) := hpri
Proof state after:
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝⁷ : Field K
inst✝⁶ : NumberField K
inst✝⁵ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
inst✝⁴ : Fintype (ClassGroup (𝓞 K))
hreg : (↑p).Coprime (Fintype.card (ClassGroup (𝓞 K)))
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
u✝ : (𝓞 K)ˣ
hcong✝ : (↑hζ.unit' - 1) ^ ↑p ∣ ↑u✝ - 1
hu : ∀ (v : K), v ^ ↑p ≠ (algebraMap (𝓞 K) K) ↑u✝
L : Type ?u.56521
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : FiniteDimensional K L
inst✝ : IsSplittingField K L (X ^ ↑p - C ((algebraMap (𝓞 K) K) ↑u✝))
σ : L ≃ₐ[K] L
hσ : ∀ (x : L ≃ₐ[K] L), x ∈ Subgroup.zpowers σ
u : (𝓞 K)ˣ
hcong : ∃ n, ↑↑p ∣ ↑u - ↑n
this : Fact (↑p).Prime
⊢ ∃ v, u = v ^ ↑p
Theorem: eq_pow_prime_of_unit_of_congruent
Proof state before:
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝⁷ : Field K
inst✝⁶ : NumberField K
inst✝⁵ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
inst✝⁴ : Fintype (ClassGroup (𝓞 K))
hreg : (↑p).Coprime (Fintype.card (ClassGroup (𝓞 K)))
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
u✝ : (𝓞 K)ˣ
hcong✝ : (↑hζ.unit' - 1) ^ ↑p ∣ ↑u✝ - 1
hu : ∀ (v : K), v ^ ↑p ≠ (algebraMap (𝓞 K) K) ↑u✝
L : Type ?u.56521
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : FiniteDimensional K L
inst✝ : IsSplittingField K L (X ^ ↑p - C ((algebraMap (𝓞 K) K) ↑u✝))
σ : L ≃ₐ[K] L
hσ : ∀ (x : L ≃ₐ[K] L), x ∈ Subgroup.zpowers σ
u : (𝓞 K)ˣ
hcong : ∃ n, ↑↑p ∣ ↑u - ↑n
this : Fact (↑p).Prime
⊢ ∃ v, u = v ^ ↑p
Tactic:
obtain ⟨ζ, hζ⟩ := IsCyclotomicExtension.exists_prim_root (S := {p}) ℚ (B := K) (n := p) rfl
Proof state after:
case intro
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝⁷ : Field K
inst✝⁶ : NumberField K
inst✝⁵ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
inst✝⁴ : Fintype (ClassGroup (𝓞 K))
hreg : (↑p).Coprime (Fintype.card (ClassGroup (𝓞 K)))
ζ✝ : K
hζ✝ : IsPrimitiveRoot ζ✝ ↑p
u✝ : (𝓞 K)ˣ
hcong✝ : (↑hζ✝.unit' - 1) ^ ↑p ∣ ↑u✝ - 1
hu : ∀ (v : K), v ^ ↑p ≠ (algebraMap (𝓞 K) K) ↑u✝
L : Type ?u.56521
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : FiniteDimensional K L
inst✝ : IsSplittingField K L (X ^ ↑p - C ((algebraMap (𝓞 K) K) ↑u✝))
σ : L ≃ₐ[K] L
hσ : ∀ (x : L ≃ₐ[K] L), x ∈ Subgroup.zpowers σ
u : (𝓞 K)ˣ
hcong : ∃ n, ↑↑p ∣ ↑u - ↑n
this : Fact (↑p).Prime
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
⊢ ∃ v, u = v ^ ↑p
Theorem: eq_pow_prime_of_unit_of_congruent
Proof state before:
case intro
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝⁷ : Field K
inst✝⁶ : NumberField K
inst✝⁵ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
inst✝⁴ : Fintype (ClassGroup (𝓞 K))
hreg : (↑p).Coprime (Fintype.card (ClassGroup (𝓞 K)))
ζ✝ : K
hζ✝ : IsPrimitiveRoot ζ✝ ↑p
u✝ : (𝓞 K)ˣ
hcong✝ : (↑hζ✝.unit' - 1) ^ ↑p ∣ ↑u✝ - 1
hu : ∀ (v : K), v ^ ↑p ≠ (algebraMap (𝓞 K) K) ↑u✝
L : Type ?u.56521
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : FiniteDimensional K L
inst✝ : IsSplittingField K L (X ^ ↑p - C ((algebraMap (𝓞 K) K) ↑u✝))
σ : L ≃ₐ[K] L
hσ : ∀ (x : L ≃ₐ[K] L), x ∈ Subgroup.zpowers σ
u : (𝓞 K)ˣ
hcong : ∃ n, ↑↑p ∣ ↑u - ↑n
this : Fact (↑p).Prime
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
⊢ ∃ v, u = v ^ ↑p
Tactic:
obtain ⟨x, hx⟩ : (p : 𝓞 K) ∣ (↑(u ^ (p - 1 : ℕ)) : 𝓞 K) - 1
Proof state after:
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝⁷ : Field K
inst✝⁶ : NumberField K
inst✝⁵ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
inst✝⁴ : Fintype (ClassGroup (𝓞 K))
hreg : (↑p).Coprime (Fintype.card (ClassGroup (𝓞 K)))
ζ✝ : K
hζ✝ : IsPrimitiveRoot ζ✝ ↑p
u✝ : (𝓞 K)ˣ
hcong✝ : (↑hζ✝.unit' - 1) ^ ↑p ∣ ↑u✝ - 1
hu : ∀ (v : K), v ^ ↑p ≠ (algebraMap (𝓞 K) K) ↑u✝
L : Type ?u.56521
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : FiniteDimensional K L
inst✝ : IsSplittingField K L (X ^ ↑p - C ((algebraMap (𝓞 K) K) ↑u✝))
σ : L ≃ₐ[K] L
hσ : ∀ (x : L ≃ₐ[K] L), x ∈ Subgroup.zpowers σ
u : (𝓞 K)ˣ
hcong : ∃ n, ↑↑p ∣ ↑u - ↑n
this : Fact (↑p).Prime
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
⊢ ↑↑p ∣ ↑(u ^ (↑p - 1)) - 1

case intro.intro
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝⁷ : Field K
inst✝⁶ : NumberField K
inst✝⁵ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
inst✝⁴ : Fintype (ClassGroup (𝓞 K))
hreg : (↑p).Coprime (Fintype.card (ClassGroup (𝓞 K)))
ζ✝ : K
hζ✝ : IsPrimitiveRoot ζ✝ ↑p
u✝ : (𝓞 K)ˣ
hcong✝ : (↑hζ✝.unit' - 1) ^ ↑p ∣ ↑u✝ - 1
hu : ∀ (v : K), v ^ ↑p ≠ (algebraMap (𝓞 K) K) ↑u✝
L : Type ?u.56521
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : FiniteDimensional K L
inst✝ : IsSplittingField K L (X ^ ↑p - C ((algebraMap (𝓞 K) K) ↑u✝))
σ : L ≃ₐ[K] L
hσ : ∀ (x : L ≃ₐ[K] L), x ∈ Subgroup.zpowers σ
u : (𝓞 K)ˣ
hcong : ∃ n, ↑↑p ∣ ↑u - ↑n
this : Fact (↑p).Prime
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
x : 𝓞 K
hx : ↑(u ^ (↑p - 1)) - 1 = ↑↑p * x
⊢ ∃ v, u = v ^ ↑p