internlm/Lean-Github huggingface dataset:
Theorem: eq_pow_prime_of_unit_of_congruent
Proof state before:
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
Tactic:
have : (hζ.unit' - 1 : 𝓞 K) ^ (p : ℕ) ∣ (↑(u ^ (p - 1 : ℕ)) : 𝓞 K) - 1
Proof state after:
case this
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
⊢ (↑hζ.unit' - 1) ^ ↑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
this : (↑hζ.unit' - 1) ^ ↑p ∣ ↑(u ^ (↑p - 1)) - 1
⊢ ∃ v, u = v ^ ↑p
Theorem: eq_pow_prime_of_unit_of_congruent
Proof state before:
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
this : (↑hζ.unit' - 1) ^ ↑p ∣ ↑(u ^ (↑p - 1)) - 1
⊢ ∃ v, u = v ^ ↑p
Tactic:
have : ¬(∀ v : K, _) := false_of_zeta_sub_one_pow_dvd_sub_one_of_pow_ne hp hreg hζ _ this
Proof state after:
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
this✝ : (↑hζ.unit' - 1) ^ ↑p ∣ ↑(u ^ (↑p - 1)) - 1
this : ¬∀ (v : K), v ^ ↑p ≠ (algebraMap (𝓞 K) K) ↑(u ^ (↑p - 1))
⊢ ∃ v, u = v ^ ↑p
Theorem: eq_pow_prime_of_unit_of_congruent
Proof state before:
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
this✝ : (↑hζ.unit' - 1) ^ ↑p ∣ ↑(u ^ (↑p - 1)) - 1
this : ¬∀ (v : K), v ^ ↑p ≠ (algebraMap (𝓞 K) K) ↑(u ^ (↑p - 1))
⊢ ∃ v, u = v ^ ↑p
Tactic:
simp only [not_forall, not_not] at this
Proof state after:
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
this✝ : (↑hζ.unit' - 1) ^ ↑p ∣ ↑(u ^ (↑p - 1)) - 1
this : ∃ x, x ^ ↑p = (algebraMap (𝓞 K) K) ↑(u ^ (↑p - 1))
⊢ ∃ v, u = v ^ ↑p
Theorem: eq_pow_prime_of_unit_of_congruent
Proof state before:
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
this✝ : (↑hζ.unit' - 1) ^ ↑p ∣ ↑(u ^ (↑p - 1)) - 1
this : ∃ x, x ^ ↑p = (algebraMap (𝓞 K) K) ↑(u ^ (↑p - 1))
⊢ ∃ v, u = v ^ ↑p
Tactic:
obtain ⟨v, hv⟩ := this
Proof state after:
case intro.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
this : (↑hζ.unit' - 1) ^ ↑p ∣ ↑(u ^ (↑p - 1)) - 1
v : K
hv : v ^ ↑p = (algebraMap (𝓞 K) K) ↑(u ^ (↑p - 1))
⊢ ∃ v, u = v ^ ↑p
Theorem: eq_pow_prime_of_unit_of_congruent
Proof state before:
case intro.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
this : (↑hζ.unit' - 1) ^ ↑p ∣ ↑(u ^ (↑p - 1)) - 1
v : K
hv : v ^ ↑p = (algebraMap (𝓞 K) K) ↑(u ^ (↑p - 1))
⊢ ∃ v, u = v ^ ↑p
Tactic:
have hv' : IsIntegral ℤ v
Proof state after:
case hv'
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
this : (↑hζ.unit' - 1) ^ ↑p ∣ ↑(u ^ (↑p - 1)) - 1
v : K
hv : v ^ ↑p = (algebraMap (𝓞 K) K) ↑(u ^ (↑p - 1))
⊢ IsIntegral ℤ v

case intro.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
this : (↑hζ.unit' - 1) ^ ↑p ∣ ↑(u ^ (↑p - 1)) - 1
v : K
hv : v ^ ↑p = (algebraMap (𝓞 K) K) ↑(u ^ (↑p - 1))
hv' : IsIntegral ℤ v
⊢ ∃ v, u = v ^ ↑p
Theorem: eq_pow_prime_of_unit_of_congruent
Proof state before:
case intro.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
this : (↑hζ.unit' - 1) ^ ↑p ∣ ↑(u ^ (↑p - 1)) - 1
v : K
hv : v ^ ↑p = (algebraMap (𝓞 K) K) ↑(u ^ (↑p - 1))
hv' : IsIntegral ℤ v
⊢ ∃ v, u = v ^ ↑p
Tactic:
set w : 𝓞 K := ⟨v, hv'⟩
Proof state after:
case intro.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
this : (↑hζ.unit' - 1) ^ ↑p ∣ ↑(u ^ (↑p - 1)) - 1
v : K
hv : v ^ ↑p = (algebraMap (𝓞 K) K) ↑(u ^ (↑p - 1))
hv' : IsIntegral ℤ v
w : 𝓞 K := ⟨v, hv'⟩
⊢ ∃ v, u = v ^ ↑p
Theorem: eq_pow_prime_of_unit_of_congruent
Proof state before:
case intro.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
this : (↑hζ.unit' - 1) ^ ↑p ∣ ↑(u ^ (↑p - 1)) - 1
v : K
hv : v ^ ↑p = (algebraMap (𝓞 K) K) ↑(u ^ (↑p - 1))
hv' : IsIntegral ℤ v
w : 𝓞 K := ⟨v, hv'⟩
⊢ ∃ v, u = v ^ ↑p
Tactic:
have : IsUnit w
Proof state after:
case this
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
this : (↑hζ.unit' - 1) ^ ↑p ∣ ↑(u ^ (↑p - 1)) - 1
v : K
hv : v ^ ↑p = (algebraMap (𝓞 K) K) ↑(u ^ (↑p - 1))
hv' : IsIntegral ℤ v
w : 𝓞 K := ⟨v, hv'⟩
⊢ IsUnit w

case intro.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
this✝ : (↑hζ.unit' - 1) ^ ↑p ∣ ↑(u ^ (↑p - 1)) - 1
v : K
hv : v ^ ↑p = (algebraMap (𝓞 K) K) ↑(u ^ (↑p - 1))
hv' : IsIntegral ℤ v
w : 𝓞 K := ⟨v, hv'⟩
this : IsUnit w
⊢ ∃ v, u = v ^ ↑p
Theorem: eq_pow_prime_of_unit_of_congruent
Proof state before:
case intro.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
this✝ : (↑hζ.unit' - 1) ^ ↑p ∣ ↑(u ^ (↑p - 1)) - 1
v : K
hv : v ^ ↑p = (algebraMap (𝓞 K) K) ↑(u ^ (↑p - 1))
hv' : IsIntegral ℤ v
w : 𝓞 K := ⟨v, hv'⟩
this : IsUnit w
⊢ ∃ v, u = v ^ ↑p
Tactic:
have hv'' : this.unit ^ (p : ℕ) = u ^ (p - 1 : ℕ)
Proof state after:
case hv''
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
this✝ : (↑hζ.unit' - 1) ^ ↑p ∣ ↑(u ^ (↑p - 1)) - 1
v : K
hv : v ^ ↑p = (algebraMap (𝓞 K) K) ↑(u ^ (↑p - 1))
hv' : IsIntegral ℤ v
w : 𝓞 K := ⟨v, hv'⟩
this : IsUnit w
⊢ this.unit ^ ↑p = u ^ (↑p - 1)

case intro.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
this✝ : (↑hζ.unit' - 1) ^ ↑p ∣ ↑(u ^ (↑p - 1)) - 1
v : K
hv : v ^ ↑p = (algebraMap (𝓞 K) K) ↑(u ^ (↑p - 1))
hv' : IsIntegral ℤ v
w : 𝓞 K := ⟨v, hv'⟩
this : IsUnit w
hv'' : this.unit ^ ↑p = u ^ (↑p - 1)
⊢ ∃ v, u = v ^ ↑p
Theorem: eq_pow_prime_of_unit_of_congruent
Proof state before:
case intro.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
this✝ : (↑hζ.unit' - 1) ^ ↑p ∣ ↑(u ^ (↑p - 1)) - 1
v : K
hv : v ^ ↑p = (algebraMap (𝓞 K) K) ↑(u ^ (↑p - 1))
hv' : IsIntegral ℤ v
w : 𝓞 K := ⟨v, hv'⟩
this : IsUnit w
hv'' : this.unit ^ ↑p = u ^ (↑p - 1)
⊢ ∃ v, u = v ^ ↑p
Tactic:
use u / this.unit
Proof state after:
case h
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
this✝ : (↑hζ.unit' - 1) ^ ↑p ∣ ↑(u ^ (↑p - 1)) - 1
v : K
hv : v ^ ↑p = (algebraMap (𝓞 K) K) ↑(u ^ (↑p - 1))
hv' : IsIntegral ℤ v
w : 𝓞 K := ⟨v, hv'⟩
this : IsUnit w
hv'' : this.unit ^ ↑p = u ^ (↑p - 1)
⊢ u = (u / this.unit) ^ ↑p
Theorem: eq_pow_prime_of_unit_of_congruent
Proof state before:
case h
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
this✝ : (↑hζ.unit' - 1) ^ ↑p ∣ ↑(u ^ (↑p - 1)) - 1
v : K
hv : v ^ ↑p = (algebraMap (𝓞 K) K) ↑(u ^ (↑p - 1))
hv' : IsIntegral ℤ v
w : 𝓞 K := ⟨v, hv'⟩
this : IsUnit w
hv'' : this.unit ^ ↑p = u ^ (↑p - 1)
⊢ u = (u / this.unit) ^ ↑p
Tactic:
rw [div_pow, hv'', div_eq_mul_inv, ← pow_sub _ tsub_le_self,
  tsub_tsub_cancel_of_le (Nat.Prime.one_lt hpri.out).le, pow_one]
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
this : Fact (↑p).Prime
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
⊢ ↑↑p ∣ ↑(u ^ (↑p - 1)) - 1
Tactic:
obtain ⟨n, hn⟩ := hcong
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)ˣ
this : Fact (↑p).Prime
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
n : ℤ
hn : ↑↑p ∣ ↑u - ↑n
⊢ ↑↑p ∣ ↑(u ^ (↑p - 1)) - 1