Theorem: false_of_zeta_sub_one_pow_dvd_sub_one_of_pow_ne (FltRegular/NumberTheory/KummersLemma/KummersLemma.lean)

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
⊢ False
Tactic:
letI := Fact.mk (X_pow_sub_C_irreducible_of_prime hpri.out hu)
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 }
⊢ False

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 }
⊢ False
Tactic:
let L := AdjoinRoot (Polynomial.X ^ (p : ℕ) - Polynomial.C (u : K))
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))
⊢ False

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))
⊢ False
Tactic:
haveI := isSplittingField_AdjoinRoot_X_pow_sub_C ⟨ζ, (mem_primitiveRoots p.pos).mpr hζ⟩
  (X_pow_sub_C_irreducible_of_prime hpri.out hu)
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))
⊢ False

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))
⊢ False
Tactic:
haveI := isGalois_of_isSplittingField_X_pow_sub_C ⟨ζ, (mem_primitiveRoots p.pos).mpr hζ⟩
  (X_pow_sub_C_irreducible_of_prime hpri.out hu) L
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
⊢ False

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
⊢ False
Tactic:
have := Polynomial.IsSplittingField.finiteDimensional L
  (Polynomial.X ^ (p : ℕ) - Polynomial.C (u : K))
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
⊢ False

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
⊢ False
Tactic:
have := isCyclic_of_isSplittingField_X_pow_sub_C ⟨ζ, (mem_primitiveRoots p.pos).mpr hζ⟩
    (X_pow_sub_C_irreducible_of_prime hpri.out hu) L
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)
⊢ False

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)
⊢ False
Tactic:
have : CharZero L := charZero_of_injective_algebraMap (algebraMap K L).injective
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
⊢ False

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
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

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 := ⟨⟩
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

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)
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

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
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

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)
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

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
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

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)
State after:
no goals

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
State after:
no goals