Theorem: eq_pow_prime_of_unit_of_congruent (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.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
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

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

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

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

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

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

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

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

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

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

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

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

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

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)ˣ
this : Fact (↑p).Prime
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
n : ℤ
hn : ↑↑p ∣ ↑u - ↑n
⊢ ↑↑p ∣ ↑(u ^ (↑p - 1)) - 1
Tactic:
have hn' : (p : ℤ) ∣ n ^ (p - 1 : ℕ) - 1
State after:
case hn'
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 ∣ n ^ (↑p - 1) - 1

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
hn' : ↑↑p ∣ n ^ (↑p - 1) - 1
⊢ ↑↑p ∣ ↑(u ^ (↑p - 1)) - 1

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)ˣ
this : Fact (↑p).Prime
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
n : ℤ
hn : ↑↑p ∣ ↑u - ↑n
hn' : ↑↑p ∣ n ^ (↑p - 1) - 1
⊢ ↑↑p ∣ ↑(u ^ (↑p - 1)) - 1
Tactic:
replace hn' := _root_.map_dvd (Int.castRingHom (𝓞 K)) hn'
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
hn' : (Int.castRingHom (𝓞 K)) ↑↑p ∣ (Int.castRingHom (𝓞 K)) (n ^ (↑p - 1) - 1)
⊢ ↑↑p ∣ ↑(u ^ (↑p - 1)) - 1

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)ˣ
this : Fact (↑p).Prime
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
n : ℤ
hn : ↑↑p ∣ ↑u - ↑n
hn' : (Int.castRingHom (𝓞 K)) ↑↑p ∣ (Int.castRingHom (𝓞 K)) (n ^ (↑p - 1) - 1)
⊢ ↑↑p ∣ ↑(u ^ (↑p - 1)) - 1
Tactic:
simp only [map_natCast, eq_intCast, Int.cast_sub, Int.cast_pow, Int.cast_one] at hn'
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
hn' : ↑↑p ∣ ↑n ^ (↑p - 1) - 1
⊢ ↑↑p ∣ ↑(u ^ (↑p - 1)) - 1

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)ˣ
this : Fact (↑p).Prime
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
n : ℤ
hn : ↑↑p ∣ ↑u - ↑n
hn' : ↑↑p ∣ ↑n ^ (↑p - 1) - 1
⊢ ↑↑p ∣ ↑(u ^ (↑p - 1)) - 1
Tactic:
rw [← Ideal.mem_span_singleton, ← Ideal.Quotient.eq_zero_iff_mem,
  RingHom.map_sub, sub_eq_zero] at hn hn' ⊢
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 : (Ideal.Quotient.mk (Ideal.span {↑↑p})) ↑u = (Ideal.Quotient.mk (Ideal.span {↑↑p})) ↑n
hn' : (Ideal.Quotient.mk (Ideal.span {↑↑p})) (↑n ^ (↑p - 1)) = (Ideal.Quotient.mk (Ideal.span {↑↑p})) 1
⊢ (Ideal.Quotient.mk (Ideal.span {↑↑p})) ↑(u ^ (↑p - 1)) = (Ideal.Quotient.mk (Ideal.span {↑↑p})) 1

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)ˣ
this : Fact (↑p).Prime
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
n : ℤ
hn : (Ideal.Quotient.mk (Ideal.span {↑↑p})) ↑u = (Ideal.Quotient.mk (Ideal.span {↑↑p})) ↑n
hn' : (Ideal.Quotient.mk (Ideal.span {↑↑p})) (↑n ^ (↑p - 1)) = (Ideal.Quotient.mk (Ideal.span {↑↑p})) 1
⊢ (Ideal.Quotient.mk (Ideal.span {↑↑p})) ↑(u ^ (↑p - 1)) = (Ideal.Quotient.mk (Ideal.span {↑↑p})) 1
Tactic:
rw [Units.val_pow_eq_pow_val, RingHom.map_pow, hn, ← RingHom.map_pow, hn']
State after:
no goals

State before:
case hn'
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 ∣ n ^ (↑p - 1) - 1
Tactic:
refine Int.modEq_iff_dvd.mp (Int.ModEq.pow_card_sub_one_eq_one hpri.out (n := n) ?_).symm
State after:
case hn'
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
⊢ IsCoprime n ↑↑p

State before:
case hn'
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
⊢ IsCoprime n ↑↑p
Tactic:
rw [isCoprime_comm, (Nat.prime_iff_prime_int.mp hpri.out).coprime_iff_not_dvd]
State after:
case hn'
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 ∣ n

State before:
case hn'
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 ∣ n
Tactic:
intro h
State after:
case hn'
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
h : ↑↑p ∣ n
⊢ False

State before:
case hn'
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
h : ↑↑p ∣ n
⊢ False
Tactic:
replace h := _root_.map_dvd (Int.castRingHom (𝓞 K)) h
State after:
case hn'
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
h : (Int.castRingHom (𝓞 K)) ↑↑p ∣ (Int.castRingHom (𝓞 K)) n
⊢ False

State before:
case hn'
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
h : (Int.castRingHom (𝓞 K)) ↑↑p ∣ (Int.castRingHom (𝓞 K)) n
⊢ False
Tactic:
simp only [map_natCast, eq_intCast, ← dvd_iff_dvd_of_dvd_sub hn] at h
State after:
case hn'
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
h : ↑↑p ∣ ↑u
⊢ False

State before:
case hn'
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
h : ↑↑p ∣ ↑u
⊢ False
Tactic:
refine hζ.zeta_sub_one_prime'.not_unit ((isUnit_pow_iff ?_).mp
  (isUnit_of_dvd_unit ((associated_zeta_sub_one_pow_prime hζ).dvd.trans h) u.isUnit))
State after:
case hn'
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
h : ↑↑p ∣ ↑u
⊢ ↑p - 1 ≠ 0

State before:
case hn'
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
h : ↑↑p ∣ ↑u
⊢ ↑p - 1 ≠ 0
Tactic:
simpa only [ge_iff_le, ne_eq, tsub_eq_zero_iff_le, not_le] using hpri.out.one_lt
State after:
no goals

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ζ.unit' - 1) ^ ↑p ∣ ↑(u ^ (↑p - 1)) - 1
Tactic:
rw [hx]
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 ∣ ↑↑p * x

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ζ.unit' - 1) ^ ↑p ∣ ↑↑p * x
Tactic:
rw [sub_eq_iff_eq_add, add_comm] at hx
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 ∣ ↑↑p * x

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ζ.unit' - 1) ^ ↑p ∣ ↑↑p * x
Tactic:
have H : Algebra.norm ℤ (1 + (p : ℕ) • x) = 1 := norm_add_one_smul_of_isUnit hpri.out
  (PNat.coe_injective.ne_iff.mpr hp) x (by rw [nsmul_eq_mul, ← hx]; exact Units.isUnit _)
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
⊢ (↑hζ.unit' - 1) ^ ↑p ∣ ↑↑p * x

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

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

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

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

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

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

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

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

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

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

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

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