internlm/Lean-Github huggingface dataset:
Theorem: eq_pow_prime_of_unit_of_congruent
Proof state before:
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 : (Algebra.norm ℤ) (1 + ↑p • x) = 1
⊢ (↑hζ.unit' - 1) ^ ↑p ∣ ↑↑p * x
Tactic:
have := H ▸ zeta_sub_one_pow_dvd_norm_sub_pow hζ x
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 : (Algebra.norm ℤ) (1 + ↑p • x) = 1
this : (↑hζ.unit' - 1) ^ ↑p ∣ ↑1 - 1 + ↑p • x
⊢ (↑hζ.unit' - 1) ^ ↑p ∣ ↑↑p * x
Theorem: eq_pow_prime_of_unit_of_congruent
Proof state before:
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 : (Algebra.norm ℤ) (1 + ↑p • x) = 1
this : (↑hζ.unit' - 1) ^ ↑p ∣ ↑1 - 1 + ↑p • x
⊢ (↑hζ.unit' - 1) ^ ↑p ∣ ↑↑p * x
Tactic:
simpa [ge_iff_le, Int.cast_one, sub_self, nsmul_eq_mul, Nat.cast_mul, PNat.pos,
  Nat.cast_pred, zero_sub, IsUnit.mul_iff, ne_eq, tsub_eq_zero_iff_le, not_le, dvd_neg,
  Units.isUnit, and_true, zero_add] using this
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
x : 𝓞 K
hx : ↑(u ^ (↑p - 1)) = 1 + ↑↑p * x
⊢ IsUnit (1 + ↑p • x)
Tactic:
rw [nsmul_eq_mul, ← hx]
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
x : 𝓞 K
hx : ↑(u ^ (↑p - 1)) = 1 + ↑↑p * x
⊢ IsUnit ↑(u ^ (↑p - 1))
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
x : 𝓞 K
hx : ↑(u ^ (↑p - 1)) = 1 + ↑↑p * x
⊢ IsUnit ↑(u ^ (↑p - 1))
Tactic:
exact Units.isUnit _
Proof state after:
no goals
Theorem: eq_pow_prime_of_unit_of_congruent
Proof state before:
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
Tactic:
apply IsIntegral.of_pow p.pos
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 ^ ↑p)
Theorem: eq_pow_prime_of_unit_of_congruent
Proof state before:
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 ^ ↑p)
Tactic:
rw [hv]
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 ℤ ((algebraMap (𝓞 K) K) ↑(u ^ (↑p - 1)))
Theorem: eq_pow_prime_of_unit_of_congruent
Proof state before:
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 ℤ ((algebraMap (𝓞 K) K) ↑(u ^ (↑p - 1)))
Tactic:
exact NumberField.RingOfIntegers.isIntegral_coe _
Proof state after:
no goals
Theorem: eq_pow_prime_of_unit_of_congruent
Proof state before:
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
Tactic:
rw [← isUnit_pow_iff p.pos.ne.symm]
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 ^ ↑p)
Theorem: eq_pow_prime_of_unit_of_congruent
Proof state before:
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 ^ ↑p)
Tactic:
convert (u ^ (p - 1 : ℕ) : (𝓞 K)ˣ).isUnit
Proof state after:
case h.e'_3
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'⟩
⊢ w ^ ↑p = ↑(u ^ (↑p - 1))
Theorem: eq_pow_prime_of_unit_of_congruent
Proof state before:
case h.e'_3
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'⟩
⊢ w ^ ↑p = ↑(u ^ (↑p - 1))
Tactic:
ext
Proof state after:
case h.e'_3.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'⟩
⊢ ↑(w ^ ↑p) = ↑↑(u ^ (↑p - 1))
Theorem: eq_pow_prime_of_unit_of_congruent
Proof state before:
case h.e'_3.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'⟩
⊢ ↑(w ^ ↑p) = ↑↑(u ^ (↑p - 1))
Tactic:
exact hv
Proof state after:
no goals
Theorem: eq_pow_prime_of_unit_of_congruent
Proof state before:
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)
Tactic:
ext
Proof state after:
case hv''.a.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
⊢ ↑↑(this.unit ^ ↑p) = ↑↑(u ^ (↑p - 1))
Theorem: eq_pow_prime_of_unit_of_congruent
Proof state before:
case hv''.a.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
⊢ ↑↑(this.unit ^ ↑p) = ↑↑(u ^ (↑p - 1))
Tactic:
simpa only [Units.val_pow_eq_pow_val, IsUnit.unit_spec, SubmonoidClass.coe_pow] using hv
Proof state after:
no goals
Theorem: MvPolynomial.Finsupp.sum_update_add
Proof state before:
R : Type ?u.11
ι : Type u_3
inst✝² : CommSemiring R
α : Type u_1
β : Type u_2
inst✝¹ : AddCommMonoid α
inst✝ : AddCommMonoid β
f : ι →₀ α
i : ι
a : α
g : ι → α → β
hg : ∀ (i : ι), g i 0 = 0
hgg : ∀ (a : ι) (b₁ b₂ : α), g a (b₁ + b₂) = g a b₁ + g a b₂
⊢ (f.update i a).sum g + g i (f i) = f.sum g + g i a
Tactic:
classical
simp_rw [Finsupp.update_eq_erase_add_single]
rw [Finsupp.sum_add_index (fun i _ => hg i) fun i _ => hgg i]
conv_rhs => rw [← Finsupp.update_self f i]
rw [Finsupp.update_eq_erase_add_single]
rw [Finsupp.sum_add_index (fun i _ => hg i) fun i _ => hgg i]
rw [add_assoc]
rw [add_assoc]
congr 1
rw [add_comm]
rw [Finsupp.sum_single_index (hg _)]
rw [Finsupp.sum_single_index (hg _)]
Proof state after:
no goals
Theorem: MvPolynomial.Finsupp.sum_update_add
Proof state before:
R : Type ?u.11
ι : Type u_3
inst✝² : CommSemiring R
α : Type u_1
β : Type u_2
inst✝¹ : AddCommMonoid α
inst✝ : AddCommMonoid β
f : ι →₀ α
i : ι
a : α
g : ι → α → β
hg : ∀ (i : ι), g i 0 = 0
hgg : ∀ (a : ι) (b₁ b₂ : α), g a (b₁ + b₂) = g a b₁ + g a b₂
⊢ (f.update i a).sum g + g i (f i) = f.sum g + g i a
Tactic:
simp_rw [Finsupp.update_eq_erase_add_single]
Proof state after:
R : Type ?u.11
ι : Type u_3
inst✝² : CommSemiring R
α : Type u_1
β : Type u_2
inst✝¹ : AddCommMonoid α
inst✝ : AddCommMonoid β
f : ι →₀ α
i : ι
a : α
g : ι → α → β
hg : ∀ (i : ι), g i 0 = 0
hgg : ∀ (a : ι) (b₁ b₂ : α), g a (b₁ + b₂) = g a b₁ + g a b₂
⊢ (Finsupp.erase i f + Finsupp.single i a).sum g + g i (f i) = f.sum g + g i a
Theorem: MvPolynomial.Finsupp.sum_update_add
Proof state before:
R : Type ?u.11
ι : Type u_3
inst✝² : CommSemiring R
α : Type u_1
β : Type u_2
inst✝¹ : AddCommMonoid α
inst✝ : AddCommMonoid β
f : ι →₀ α
i : ι
a : α
g : ι → α → β
hg : ∀ (i : ι), g i 0 = 0
hgg : ∀ (a : ι) (b₁ b₂ : α), g a (b₁ + b₂) = g a b₁ + g a b₂
⊢ (Finsupp.erase i f + Finsupp.single i a).sum g + g i (f i) = f.sum g + g i a
Tactic:
rw [Finsupp.sum_add_index (fun i _ => hg i) fun i _ => hgg i]
Proof state after:
R : Type ?u.11
ι : Type u_3
inst✝² : CommSemiring R
α : Type u_1
β : Type u_2
inst✝¹ : AddCommMonoid α
inst✝ : AddCommMonoid β
f : ι →₀ α
i : ι
a : α
g : ι → α → β
hg : ∀ (i : ι), g i 0 = 0
hgg : ∀ (a : ι) (b₁ b₂ : α), g a (b₁ + b₂) = g a b₁ + g a b₂
⊢ (((Finsupp.erase i f).sum fun i => g i) + (Finsupp.single i a).sum fun i => g i) + g i (f i) = f.sum g + g i a
Theorem: MvPolynomial.Finsupp.sum_update_add
Proof state before:
R : Type ?u.11
ι : Type u_3
inst✝² : CommSemiring R
α : Type u_1
β : Type u_2
inst✝¹ : AddCommMonoid α
inst✝ : AddCommMonoid β
f : ι →₀ α
i : ι
a : α
g : ι → α → β
hg : ∀ (i : ι), g i 0 = 0
hgg : ∀ (a : ι) (b₁ b₂ : α), g a (b₁ + b₂) = g a b₁ + g a b₂
⊢ (((Finsupp.erase i f).sum fun i => g i) + (Finsupp.single i a).sum fun i => g i) + g i (f i) = f.sum g + g i a
Tactic:
conv_rhs => rw [← Finsupp.update_self f i]
Proof state after:
R : Type ?u.11
ι : Type u_3
inst✝² : CommSemiring R
α : Type u_1
β : Type u_2
inst✝¹ : AddCommMonoid α
inst✝ : AddCommMonoid β
f : ι →₀ α
i : ι
a : α
g : ι → α → β
hg : ∀ (i : ι), g i 0 = 0
hgg : ∀ (a : ι) (b₁ b₂ : α), g a (b₁ + b₂) = g a b₁ + g a b₂
⊢ (((Finsupp.erase i f).sum fun i => g i) + (Finsupp.single i a).sum fun i => g i) + g i (f i) =
    (f.update i (f i)).sum g + g i a
Theorem: MvPolynomial.Finsupp.sum_update_add
Proof state before:
R : Type ?u.11
ι : Type u_3
inst✝² : CommSemiring R
α : Type u_1
β : Type u_2
inst✝¹ : AddCommMonoid α
inst✝ : AddCommMonoid β
f : ι →₀ α
i : ι
a : α
g : ι → α → β
hg : ∀ (i : ι), g i 0 = 0
hgg : ∀ (a : ι) (b₁ b₂ : α), g a (b₁ + b₂) = g a b₁ + g a b₂
⊢ (((Finsupp.erase i f).sum fun i => g i) + (Finsupp.single i a).sum fun i => g i) + g i (f i) =
    (f.update i (f i)).sum g + g i a
Tactic:
rw [Finsupp.update_eq_erase_add_single]
Proof state after:
R : Type ?u.11
ι : Type u_3
inst✝² : CommSemiring R
α : Type u_1
β : Type u_2
inst✝¹ : AddCommMonoid α
inst✝ : AddCommMonoid β
f : ι →₀ α
i : ι
a : α
g : ι → α → β
hg : ∀ (i : ι), g i 0 = 0
hgg : ∀ (a : ι) (b₁ b₂ : α), g a (b₁ + b₂) = g a b₁ + g a b₂
⊢ (((Finsupp.erase i f).sum fun i => g i) + (Finsupp.single i a).sum fun i => g i) + g i (f i) =
    (Finsupp.erase i f + Finsupp.single i (f i)).sum g + g i a