awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Basic (goal)
Goal:
n₁ n₂ : ℕ
hn₁ : 1 < n₁
hn₂ : 1 < n₂
h : n₁.Coprime n₂
K : Type u
inst : Field K
inst_1 : CharZero K
hn : NeZero (n₁ * n₂)
hK : IsCyclotomicExtension {n₁ * n₂} ℚ K
this_1 : NumberField K
this_2 : NeZero n₁
this_3 : NeZero n₂
ζ : K := zeta (n₁ * n₂) ℚ K
hζ : IsPrimitiveRoot (zeta (n₁ * n₂) ℚ K) (n₁ * n₂)
hζ₁ : IsPrimitiveRoot (zeta (n₁ * n₂) ℚ K ^ n₂) n₁
this_4 : IsCyclotomicExtension.{0, u} {n₁} ℚ ↥ℚ⟮zeta (n₁ * n₂) ℚ K ^ n₂⟯
hζ₁' : IsPrimitiveRoot (M := ↥ℚ⟮ζ ^ n₂⟯) (AdjoinSimple.gen ℚ (ζ ^ n₂)) n₁
hK₁ : (NumberField.discr.{u} ↥ℚ⟮ζ ^ n₂⟯).natAbs = n₁ ^ φ n₁ / ∏ p ∈ n₁.primeFactors, p ^ (φ n₁ / (p - 1))
hζ₂ : IsPrimitiveRoot (zeta (n₁ * n₂) ℚ K ^ n₁) n₂
this_5 : IsCyclotomicExtension.{0, u} {n₂} ℚ ↥ℚ⟮zeta (n₁ * n₂) ℚ K ^ n₁⟯
hζ₂' : IsPrimitiveRoot (M := ↥ℚ⟮ζ ^ n₁⟯) (AdjoinSimple.gen ℚ (ζ ^ n₁)) n₂
hK₂ : (NumberField.discr.{u} ↥ℚ⟮ζ ^ n₁⟯).natAbs = n₂ ^ φ n₂ / ∏ p ∈ n₂.primeFactors, p ^ (φ n₂ / (p - 1))
this_6 : IsGalois.{0, u} ℚ ↥ℚ⟮ζ ^ n₂⟯
h_top : Eq (α := IntermediateField ℚ K) (ℚ⟮ζ ^ n₂⟯ ⊔ ℚ⟮ζ ^ n₁⟯) ⊤
h_cpr : IsCoprime (NumberField.discr.{u} ↥ℚ⟮ζ ^ n₂⟯) (NumberField.discr.{u} ↥ℚ⟮ζ ^ n₁⟯)
h_dsj : IntermediateField.LinearDisjoint (E := K) ℚ⟮ζ ^ n₂⟯ ↥ℚ⟮ζ ^ n₁⟯
h_div₁ : ∏ p ∈ n₁.primeFactors, p ^ (φ n₁ / (p - 1)) ∣ n₁ ^ φ n₁
h_div₂ : ∏ p ∈ n₂.primeFactors, p ^ (φ n₂ / (p - 1)) ∣ n₂ ^ φ n₂
this : ∀ {n p : ℕ} (hp : p ∈ n.primeFactors), p - 1 ∣ φ n
⊢ n₁ ^ (φ n₁ * φ n₂) * n₂ ^ (φ n₂ * φ n₁) /
      HMul.hMul (α := ℕ) (∏ x ∈ n₁.primeFactors, x ^ (φ n₁ * φ n₂ / (x - 1)))
        (∏ x ∈ n₂.primeFactors, x ^ (φ n₂ * φ n₁ / (x - 1))) =
    (n₁ * n₂) ^ (φ n₁ * φ n₂) /
      HMul.hMul (α := ℕ) (∏ x ∈ n₁.primeFactors, x ^ (φ n₁ * φ n₂ / (x - 1)))
        (∏ x ∈ n₂.primeFactors, x ^ (φ n₁ * φ n₂ / (x - 1)))
have e_a : n₁ ^ (φ n₁ * φ n₂) * n₂ ^ (φ n₂ * φ n₁) /
    HMul.hMul (α := ℕ) (∏ x ∈ n₁.primeFactors, x ^ (φ n₁ * φ n₂ / (x - 1)))
      (∏ x ∈ n₂.primeFactors, x ^ (φ n₂ * φ n₁ / (x - 1))) =
  n₁ ^ (φ n₁ * φ n₂) * n₂ ^ (φ n₁ * φ n₂) /
    HMul.hMul (α := ℕ) (∏ x ∈ n₁.primeFactors, x ^ (φ n₁ * φ n₂ / (x - 1)))
      (∏ x ∈ n₂.primeFactors, x ^ (φ n₁ * φ n₂ / (x - 1)))
Tactic: rw [mul_pow, mul_comm n₂.totient]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Basic (goal)
Goal:
n₁ n₂ : ℕ
hn₁ : 1 < n₁
hn₂ : 1 < n₂
h : n₁.Coprime n₂
K : Type u
inst : Field K
inst_1 : CharZero K
hn : NeZero (n₁ * n₂)
hK : IsCyclotomicExtension {n₁ * n₂} ℚ K
this_1 : NumberField K
this_2 : NeZero n₁
this_3 : NeZero n₂
ζ : K := zeta (n₁ * n₂) ℚ K
hζ : IsPrimitiveRoot (zeta (n₁ * n₂) ℚ K) (n₁ * n₂)
hζ₁ : IsPrimitiveRoot (zeta (n₁ * n₂) ℚ K ^ n₂) n₁
this_4 : IsCyclotomicExtension.{0, u} {n₁} ℚ ↥ℚ⟮zeta (n₁ * n₂) ℚ K ^ n₂⟯
hζ₁' : IsPrimitiveRoot (M := ↥ℚ⟮ζ ^ n₂⟯) (AdjoinSimple.gen ℚ (ζ ^ n₂)) n₁
hK₁ : (NumberField.discr.{u} ↥ℚ⟮ζ ^ n₂⟯).natAbs = n₁ ^ φ n₁ / ∏ p ∈ n₁.primeFactors, p ^ (φ n₁ / (p - 1))
hζ₂ : IsPrimitiveRoot (zeta (n₁ * n₂) ℚ K ^ n₁) n₂
this_5 : IsCyclotomicExtension.{0, u} {n₂} ℚ ↥ℚ⟮zeta (n₁ * n₂) ℚ K ^ n₁⟯
hζ₂' : IsPrimitiveRoot (M := ↥ℚ⟮ζ ^ n₁⟯) (AdjoinSimple.gen ℚ (ζ ^ n₁)) n₂
hK₂ : (NumberField.discr.{u} ↥ℚ⟮ζ ^ n₁⟯).natAbs = n₂ ^ φ n₂ / ∏ p ∈ n₂.primeFactors, p ^ (φ n₂ / (p - 1))
this_6 : IsGalois.{0, u} ℚ ↥ℚ⟮ζ ^ n₂⟯
h_top : Eq (α := IntermediateField ℚ K) (ℚ⟮ζ ^ n₂⟯ ⊔ ℚ⟮ζ ^ n₁⟯) ⊤
h_cpr : IsCoprime (NumberField.discr.{u} ↥ℚ⟮ζ ^ n₂⟯) (NumberField.discr.{u} ↥ℚ⟮ζ ^ n₁⟯)
h_dsj : IntermediateField.LinearDisjoint (E := K) ℚ⟮ζ ^ n₂⟯ ↥ℚ⟮ζ ^ n₁⟯
h_div₁ : ∏ p ∈ n₁.primeFactors, p ^ (φ n₁ / (p - 1)) ∣ n₁ ^ φ n₁
h_div₂ : ∏ p ∈ n₂.primeFactors, p ^ (φ n₂ / (p - 1)) ∣ n₂ ^ φ n₂
this : ∀ {n p : ℕ} (hp : p ∈ n.primeFactors), p - 1 ∣ φ n
e_a :
  n₁ ^ (φ n₁ * φ n₂) * n₂ ^ (φ n₂ * φ n₁) /
      HMul.hMul (α := ℕ) (∏ x ∈ n₁.primeFactors, x ^ (φ n₁ * φ n₂ / (x - 1)))
        (∏ x ∈ n₂.primeFactors, x ^ (φ n₂ * φ n₁ / (x - 1))) =
    n₁ ^ (φ n₁ * φ n₂) * n₂ ^ (φ n₁ * φ n₂) /
      HMul.hMul (α := ℕ) (∏ x ∈ n₁.primeFactors, x ^ (φ n₁ * φ n₂ / (x - 1)))
        (∏ x ∈ n₂.primeFactors, x ^ (φ n₁ * φ n₂ / (x - 1)))
⊢ n₁ ^ (φ n₁ * φ n₂) * n₂ ^ (φ n₂ * φ n₁) /
      HMul.hMul (α := ℕ) (∏ x ∈ n₁.primeFactors, x ^ (φ n₁ * φ n₂ / (x - 1)))
        (∏ x ∈ n₂.primeFactors, x ^ (φ n₂ * φ n₁ / (x - 1))) =
    (n₁ * n₂) ^ (φ n₁ * φ n₂) /
      HMul.hMul (α := ℕ) (∏ x ∈ n₁.primeFactors, x ^ (φ n₁ * φ n₂ / (x - 1)))
        (∏ x ∈ n₂.primeFactors, x ^ (φ n₁ * φ n₂ / (x - 1)))
have e_a₁ : n₁ ^ (φ n₁ * φ n₂) * n₂ ^ (φ n₁ * φ n₂) /
    HMul.hMul (α := ℕ) (∏ x ∈ n₁.primeFactors, x ^ (φ n₁ * φ n₂ / (x - 1)))
      (∏ x ∈ n₂.primeFactors, x ^ (φ n₁ * φ n₂ / (x - 1))) =
  n₁ ^ (φ n₁ * φ n₂) * n₂ ^ (φ n₁ * φ n₂) /
    HMul.hMul (α := ℕ) (∏ x ∈ n₁.primeFactors, x ^ (φ n₁ * φ n₂ / (x - 1)))
      (∏ x ∈ n₂.primeFactors, x ^ (φ n₁ * φ n₂ / (x - 1)))
Tactic: rw [mul_pow, mul_comm n₂.totient]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Basic (hypothesis)
Goal:
n : ℕ
K : Type u
inst : Field K
inst_1 : CharZero K
hn : NeZero n
hK : IsCyclotomicExtension {n} ℚ K
⊢ (NumberField.discr K).natAbs = n ^ φ n / ∏ p ∈ n.primeFactors, p ^ (φ n / (p - 1))
have this : NumberField K
Tactic: have : NumberField K := IsCyclotomicExtension.numberField {n} ℚ K
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Basic (goal)
Goal:
n : ℕ
K : Type u
inst : Field K
inst_1 : CharZero K
hn : NeZero n
hK : IsCyclotomicExtension {n} ℚ K
this : NumberField K
⊢ (NumberField.discr K).natAbs = n ^ φ n / ∏ p ∈ n.primeFactors, p ^ (φ n / (p - 1))
have rw : (↑(∏ p ∈ n.primeFactors, p ^ (φ n / (p - 1))) : ℤ) ∣ HPow.hPow (α := ℤ) (↑n : ℤ) (φ n)
Tactic: rw [discr n K, Int.natAbs_mul, Int.natAbs_pow, Int.natAbs_neg, Int.natAbs_one, one_pow, one_mul,
    Int.natAbs_ediv_of_dvd, Int.natAbs_pow, Int.natAbs_natCast, Int.natAbs_natCast]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Basic (goal)
Goal:
n : ℕ
K : Type u
inst : Field K
inst_1 : CharZero K
hn : NeZero n
hK : IsCyclotomicExtension {n} ℚ K
this : NumberField K
⊢ (↑(∏ p ∈ n.primeFactors, p ^ (φ n / (p - 1))) : ℤ) ∣ HPow.hPow (α := ℤ) (↑n : ℤ) (φ n)
have rw : ∏ p ∈ n.primeFactors, p ^ (φ n / (p - 1)) ∣ n ^ φ n
Tactic: rw [← Nat.cast_pow, Int.natCast_dvd_natCast]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Basic (goal)
Goal:
K : Type u
inst : Field K
inst_1 : CharZero K
inst_2 : NumberField K
F₁ F₂ : IntermediateField ℚ K
n₁ n₂ : ℕ
inst_3 : NeZero n₁
inst_4 : NeZero n₂
inst_5 : IsCyclotomicExtension.{0, u} {n₁} ℚ ↥F₁
inst_6 : IsCyclotomicExtension.{0, u} {n₂} ℚ ↥F₂
ζ₁ : ↥F₁
hζ₁ : IsPrimitiveRoot ζ₁ n₁
h₁ : Eq (α := Subalgebra ℤ (𝓞 ↥F₁)) ℤ[hζ₁.toInteger] ⊤
ζ₂ : ↥F₂
hζ₂ : IsPrimitiveRoot ζ₂ n₂
h₂ : Eq (α := Subalgebra ℤ (𝓞 ↥F₂)) ℤ[hζ₂.toInteger] ⊤
h : n₁.Coprime n₂
htop : F₁ ⊔ F₂ = ⊤
ζ : K
hζ : IsPrimitiveRoot ζ (n₁ * n₂)
⊢ IsCoprime (NumberField.discr.{u} ↥F₁) (NumberField.discr.{u} ↥F₂)
have rw : (n₁ ^ φ n₁ / ∏ p ∈ n₁.primeFactors, p ^ (φ n₁ / (p - 1))).Coprime
  (n₂ ^ φ n₂ / ∏ p ∈ n₂.primeFactors, p ^ (φ n₂ / (p - 1)))
Tactic: rw [Int.isCoprime_iff_nat_coprime, natAbs_discr n₁ F₁, natAbs_discr n₂ F₂]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Basic (goal)
Goal:
K : Type u
inst : Field K
inst_1 : CharZero K
inst_2 : NumberField K
F₁ F₂ : IntermediateField ℚ K
n₁ n₂ : ℕ
inst_3 : NeZero n₁
inst_4 : NeZero n₂
inst_5 : IsCyclotomicExtension.{0, u} {n₁} ℚ ↥F₁
inst_6 : IsCyclotomicExtension.{0, u} {n₂} ℚ ↥F₂
ζ₁ : ↥F₁
hζ₁ : IsPrimitiveRoot ζ₁ n₁
h₁ : Eq (α := Subalgebra ℤ (𝓞 ↥F₁)) ℤ[hζ₁.toInteger] ⊤
ζ₂ : ↥F₂
hζ₂ : IsPrimitiveRoot ζ₂ n₂
h₂ : Eq (α := Subalgebra ℤ (𝓞 ↥F₂)) ℤ[hζ₂.toInteger] ⊤
h : n₁.Coprime n₂
htop : F₁ ⊔ F₂ = ⊤
ζ : K
hζ : IsPrimitiveRoot ζ (n₁ * n₂)
⊢ (n₁ ^ φ n₁ / ∏ p ∈ n₁.primeFactors, p ^ (φ n₁ / (p - 1))).Coprime
    (n₂ ^ φ n₂ / ∏ p ∈ n₂.primeFactors, p ^ (φ n₂ / (p - 1)))
have refine : (n₁ ^ φ n₁).Coprime (n₂ ^ φ n₂ / ∏ p ∈ n₂.primeFactors, p ^ (φ n₂ / (p - 1)))
Tactic: refine Coprime.coprime_div_left ?_ (prod_primeFactors_pow_totient_ediv_dvd (NeZero.pos _))
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Basic (goal)
Goal:
K : Type u
inst : Field K
inst_1 : CharZero K
inst_2 : NumberField K
F₁ F₂ : IntermediateField ℚ K
n₁ n₂ : ℕ
inst_3 : NeZero n₁
inst_4 : NeZero n₂
inst_5 : IsCyclotomicExtension.{0, u} {n₁} ℚ ↥F₁
inst_6 : IsCyclotomicExtension.{0, u} {n₂} ℚ ↥F₂
ζ₁ : ↥F₁
hζ₁ : IsPrimitiveRoot ζ₁ n₁
h₁ : Eq (α := Subalgebra ℤ (𝓞 ↥F₁)) ℤ[hζ₁.toInteger] ⊤
ζ₂ : ↥F₂
hζ₂ : IsPrimitiveRoot ζ₂ n₂
h₂ : Eq (α := Subalgebra ℤ (𝓞 ↥F₂)) ℤ[hζ₂.toInteger] ⊤
h : n₁.Coprime n₂
htop : F₁ ⊔ F₂ = ⊤
ζ : K
hζ : IsPrimitiveRoot ζ (n₁ * n₂)
⊢ (n₁ ^ φ n₁).Coprime (n₂ ^ φ n₂ / ∏ p ∈ n₂.primeFactors, p ^ (φ n₂ / (p - 1)))
have refine : (n₁ ^ φ n₁).Coprime (n₂ ^ φ n₂)
Tactic: refine Coprime.coprime_div_right ?_ (prod_primeFactors_pow_totient_ediv_dvd (NeZero.pos _))
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Basic (hypothesis)
Goal:
K : Type u
inst : Field K
inst_1 : CharZero K
inst_2 : NumberField K
F₁ F₂ : IntermediateField ℚ K
n₁ n₂ : ℕ
inst_3 : NeZero n₁
inst_4 : NeZero n₂
inst_5 : IsCyclotomicExtension.{0, u} {n₁} ℚ ↥F₁
inst_6 : IsCyclotomicExtension.{0, u} {n₂} ℚ ↥F₂
ζ₁ : ↥F₁
hζ₁ : IsPrimitiveRoot ζ₁ n₁
h₁ : Eq (α := Subalgebra ℤ (𝓞 ↥F₁)) ℤ[hζ₁.toInteger] ⊤
ζ₂ : ↥F₂
hζ₂ : IsPrimitiveRoot ζ₂ n₂
h₂ : Eq (α := Subalgebra ℤ (𝓞 ↥F₂)) ℤ[hζ₂.toInteger] ⊤
h : n₁.Coprime n₂
htop : F₁ ⊔ F₂ = ⊤
ζ : K
hζ : IsPrimitiveRoot ζ (n₁ * n₂)
⊢ Eq (α := Subalgebra ℤ (𝓞 K)) ℤ[hζ.toInteger] ⊤
have h_cpr : IsCoprime (NumberField.discr.{u} ↥F₁) (NumberField.discr.{u} ↥F₂)
Tactic: have h_cpr : IsCoprime (NumberField.discr F₁) (NumberField.discr F₂) := by
    rw [Int.isCoprime_iff_nat_coprime, natAbs_discr n₁ F₁, natAbs_discr n₂ F₂]
    refine Coprime.coprime_div_left ?_ (prod_primeFactors_pow_totient_ediv_dvd (NeZero.pos _))
    refine Coprime.coprime_div_right ?_ (prod_primeFactors_pow_totient_ediv_dvd (NeZero.pos _))
    exact Coprime.pow_left _ (Coprime.pow_right _ h)
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Basic (hypothesis)
Goal:
K : Type u
inst : Field K
inst_1 : CharZero K
inst_2 : NumberField K
F₁ F₂ : IntermediateField ℚ K
n₁ n₂ : ℕ
inst_3 : NeZero n₁
inst_4 : NeZero n₂
inst_5 : IsCyclotomicExtension.{0, u} {n₁} ℚ ↥F₁
inst_6 : IsCyclotomicExtension.{0, u} {n₂} ℚ ↥F₂
ζ₁ : ↥F₁
hζ₁ : IsPrimitiveRoot ζ₁ n₁
h₁ : Eq (α := Subalgebra ℤ (𝓞 ↥F₁)) ℤ[hζ₁.toInteger] ⊤
ζ₂ : ↥F₂
hζ₂ : IsPrimitiveRoot ζ₂ n₂
h₂ : Eq (α := Subalgebra ℤ (𝓞 ↥F₂)) ℤ[hζ₂.toInteger] ⊤
h : n₁.Coprime n₂
htop : F₁ ⊔ F₂ = ⊤
ζ : K
hζ : IsPrimitiveRoot ζ (n₁ * n₂)
h_cpr : IsCoprime (NumberField.discr.{u} ↥F₁) (NumberField.discr.{u} ↥F₂)
⊢ F₁.LinearDisjoint ↥F₂
have this : IsGalois.{0, u} ℚ ↥F₁
Tactic: have : IsGalois ℚ F₁ := IsCyclotomicExtension.isGalois {n₁} ℚ F₁
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Basic (hypothesis)
Goal:
K : Type u
inst : Field K
inst_1 : CharZero K
inst_2 : NumberField K
F₁ F₂ : IntermediateField ℚ K
n₁ n₂ : ℕ
inst_3 : NeZero n₁
inst_4 : NeZero n₂
inst_5 : IsCyclotomicExtension.{0, u} {n₁} ℚ ↥F₁
inst_6 : IsCyclotomicExtension.{0, u} {n₂} ℚ ↥F₂
ζ₁ : ↥F₁
hζ₁ : IsPrimitiveRoot ζ₁ n₁
h₁ : Eq (α := Subalgebra ℤ (𝓞 ↥F₁)) ℤ[hζ₁.toInteger] ⊤
ζ₂ : ↥F₂
hζ₂ : IsPrimitiveRoot ζ₂ n₂
h₂ : Eq (α := Subalgebra ℤ (𝓞 ↥F₂)) ℤ[hζ₂.toInteger] ⊤
h : n₁.Coprime n₂
htop : F₁ ⊔ F₂ = ⊤
ζ : K
hζ : IsPrimitiveRoot ζ (n₁ * n₂)
h_cpr : IsCoprime (NumberField.discr.{u} ↥F₁) (NumberField.discr.{u} ↥F₂)
⊢ Eq (α := Subalgebra ℤ (𝓞 K)) ℤ[hζ.toInteger] ⊤
have h_disj : F₁.LinearDisjoint ↥F₂
Tactic: have h_disj : F₁.LinearDisjoint F₂ := by
    have : IsGalois ℚ F₁ := IsCyclotomicExtension.isGalois {n₁} ℚ F₁
    apply linearDisjoint_of_isGalois_isCoprime_discr
    exact h_cpr
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Basic (hypothesis)
Goal:
K : Type u
inst : Field K
inst_1 : CharZero K
inst_2 : NumberField K
F₁ F₂ : IntermediateField ℚ K
n₁ n₂ : ℕ
inst_3 : NeZero n₁
inst_4 : NeZero n₂
inst_5 : IsCyclotomicExtension.{0, u} {n₁} ℚ ↥F₁
inst_6 : IsCyclotomicExtension.{0, u} {n₂} ℚ ↥F₂
ζ₁ : ↥F₁
hζ₁ : IsPrimitiveRoot ζ₁ n₁
h₁ : Eq (α := Subalgebra ℤ (𝓞 ↥F₁)) ℤ[hζ₁.toInteger] ⊤
ζ₂ : ↥F₂
hζ₂ : IsPrimitiveRoot ζ₂ n₂
h₂ : Eq (α := Subalgebra ℤ (𝓞 ↥F₂)) ℤ[hζ₂.toInteger] ⊤
h : n₁.Coprime n₂
htop : F₁ ⊔ F₂ = ⊤
ζ : K
hζ : IsPrimitiveRoot ζ (n₁ * n₂)
h_cpr : IsCoprime (NumberField.discr.{u} ↥F₁) (NumberField.discr.{u} ↥F₂)
h_disj : F₁.LinearDisjoint ↥F₂
⊢ Eq (α := Subalgebra ℤ (𝓞 K)) ℤ[hζ.toInteger] ⊤
have hζ₃ : IsPrimitiveRoot hζ₁.toInteger n₁
Tactic: replace hζ₁ : IsPrimitiveRoot hζ₁.toInteger n₁ := hζ₁.toInteger_isPrimitiveRoot
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Basic (hypothesis)
Goal:
K : Type u
inst : Field K
inst_1 : CharZero K
inst_2 : NumberField K
F₁ F₂ : IntermediateField ℚ K
n₁ n₂ : ℕ
inst_3 : NeZero n₁
inst_4 : NeZero n₂
inst_5 : IsCyclotomicExtension.{0, u} {n₁} ℚ ↥F₁
inst_6 : IsCyclotomicExtension.{0, u} {n₂} ℚ ↥F₂
ζ₁ : ↥F₁
hζ₁_1 : IsPrimitiveRoot ζ₁ n₁
h₁ : Eq (α := Subalgebra ℤ (𝓞 ↥F₁)) ℤ[hζ₁_1.toInteger] ⊤
ζ₂ : ↥F₂
hζ₂ : IsPrimitiveRoot ζ₂ n₂
h₂ : Eq (α := Subalgebra ℤ (𝓞 ↥F₂)) ℤ[hζ₂.toInteger] ⊤
h : n₁.Coprime n₂
htop : F₁ ⊔ F₂ = ⊤
ζ : K
hζ : IsPrimitiveRoot ζ (n₁ * n₂)
h_cpr : IsCoprime (NumberField.discr.{u} ↥F₁) (NumberField.discr.{u} ↥F₂)
h_disj : F₁.LinearDisjoint ↥F₂
hζ₁ : IsPrimitiveRoot hζ₁_1.toInteger n₁
⊢ Eq (α := Subalgebra ℤ (𝓞 K)) ℤ[hζ.toInteger] ⊤
have hζ₃ : IsPrimitiveRoot (M := 𝓞 K) ((algebraMap (𝓞 ↥F₁) (𝓞 K) : (a : 𝓞 ↥F₁) → 𝓞 K) hζ₁_1.toInteger : 𝓞 K) n₁
Tactic: replace hζ₁ := hζ₁.map_of_injective (FaithfulSMul.algebraMap_injective (𝓞 F₁) (𝓞 K))
Cleared hypotheses: hζ₁
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Basic (hypothesis)
Goal:
K : Type u
inst : Field K
inst_1 : CharZero K
inst_2 : NumberField K
F₁ F₂ : IntermediateField ℚ K
n₁ n₂ : ℕ
inst_3 : NeZero n₁
inst_4 : NeZero n₂
inst_5 : IsCyclotomicExtension.{0, u} {n₁} ℚ ↥F₁
inst_6 : IsCyclotomicExtension.{0, u} {n₂} ℚ ↥F₂
ζ₁ : ↥F₁
hζ₁_1 : IsPrimitiveRoot ζ₁ n₁
h₁ : Eq (α := Subalgebra ℤ (𝓞 ↥F₁)) ℤ[hζ₁_1.toInteger] ⊤
ζ₂ : ↥F₂
hζ₂ : IsPrimitiveRoot ζ₂ n₂
h₂ : Eq (α := Subalgebra ℤ (𝓞 ↥F₂)) ℤ[hζ₂.toInteger] ⊤
h : n₁.Coprime n₂
htop : F₁ ⊔ F₂ = ⊤
ζ : K
hζ : IsPrimitiveRoot ζ (n₁ * n₂)
h_cpr : IsCoprime (NumberField.discr.{u} ↥F₁) (NumberField.discr.{u} ↥F₂)
h_disj : F₁.LinearDisjoint ↥F₂
hζ₁ : IsPrimitiveRoot (M := 𝓞 K) ((algebraMap (𝓞 ↥F₁) (𝓞 K) : (a : 𝓞 ↥F₁) → 𝓞 K) hζ₁_1.toInteger : 𝓞 K) n₁
⊢ Eq (α := Subalgebra ℤ (𝓞 K)) ℤ[hζ.toInteger] ⊤
have hζ₃ : IsPrimitiveRoot hζ₂.toInteger n₂
Tactic: replace hζ₂ : IsPrimitiveRoot hζ₂.toInteger n₂ := hζ₂.toInteger_isPrimitiveRoot
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Basic (hypothesis)
Goal:
K : Type u
inst : Field K
inst_1 : CharZero K
inst_2 : NumberField K
F₁ F₂ : IntermediateField ℚ K
n₁ n₂ : ℕ
inst_3 : NeZero n₁
inst_4 : NeZero n₂
inst_5 : IsCyclotomicExtension.{0, u} {n₁} ℚ ↥F₁
inst_6 : IsCyclotomicExtension.{0, u} {n₂} ℚ ↥F₂
ζ₁ : ↥F₁
hζ₁_1 : IsPrimitiveRoot ζ₁ n₁
h₁ : Eq (α := Subalgebra ℤ (𝓞 ↥F₁)) ℤ[hζ₁_1.toInteger] ⊤
ζ₂ : ↥F₂
hζ₂_1 : IsPrimitiveRoot ζ₂ n₂
h₂ : Eq (α := Subalgebra ℤ (𝓞 ↥F₂)) ℤ[hζ₂_1.toInteger] ⊤
h : n₁.Coprime n₂
htop : F₁ ⊔ F₂ = ⊤
ζ : K
hζ : IsPrimitiveRoot ζ (n₁ * n₂)
h_cpr : IsCoprime (NumberField.discr.{u} ↥F₁) (NumberField.discr.{u} ↥F₂)
h_disj : F₁.LinearDisjoint ↥F₂
hζ₁ : IsPrimitiveRoot (M := 𝓞 K) ((algebraMap (𝓞 ↥F₁) (𝓞 K) : (a : 𝓞 ↥F₁) → 𝓞 K) hζ₁_1.toInteger : 𝓞 K) n₁
hζ₂ : IsPrimitiveRoot hζ₂_1.toInteger n₂
⊢ Eq (α := Subalgebra ℤ (𝓞 K)) ℤ[hζ.toInteger] ⊤
have hζ₃ : IsPrimitiveRoot (M := 𝓞 K) ((algebraMap (𝓞 ↥F₂) (𝓞 K) : (a : 𝓞 ↥F₂) → 𝓞 K) hζ₂_1.toInteger : 𝓞 K) n₂
Tactic: replace hζ₂ := hζ₂.map_of_injective (FaithfulSMul.algebraMap_injective (𝓞 F₂) (𝓞 K))
Cleared hypotheses: hζ₂
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Basic (goal)
Goal:
K : Type u
inst : Field K
inst_1 : CharZero K
inst_2 : NumberField K
F₁ F₂ : IntermediateField ℚ K
n₁ n₂ : ℕ
inst_3 : NeZero n₁
inst_4 : NeZero n₂
inst_5 : IsCyclotomicExtension.{0, u} {n₁} ℚ ↥F₁
inst_6 : IsCyclotomicExtension.{0, u} {n₂} ℚ ↥F₂
ζ₁ : ↥F₁
hζ₁_1 : IsPrimitiveRoot ζ₁ n₁
h₁ : Eq (α := Subalgebra ℤ (𝓞 ↥F₁)) ℤ[hζ₁_1.toInteger] ⊤
ζ₂ : ↥F₂
hζ₂_1 : IsPrimitiveRoot ζ₂ n₂
h₂ : Eq (α := Subalgebra ℤ (𝓞 ↥F₂)) ℤ[hζ₂_1.toInteger] ⊤
h : n₁.Coprime n₂
htop : F₁ ⊔ F₂ = ⊤
ζ : K
hζ : IsPrimitiveRoot ζ (n₁ * n₂)
h_cpr : IsCoprime (NumberField.discr.{u} ↥F₁) (NumberField.discr.{u} ↥F₂)
h_disj : F₁.LinearDisjoint ↥F₂
hζ₁ : IsPrimitiveRoot (M := 𝓞 K) ((algebraMap (𝓞 ↥F₁) (𝓞 K) : (a : 𝓞 ↥F₁) → 𝓞 K) hζ₁_1.toInteger : 𝓞 K) n₁
hζ₂ : IsPrimitiveRoot (M := 𝓞 K) ((algebraMap (𝓞 ↥F₂) (𝓞 K) : (a : 𝓞 ↥F₂) → 𝓞 K) hζ₂_1.toInteger : 𝓞 K) n₂
⊢ Eq (α := Subalgebra ℤ (𝓞 K)) ℤ[hζ.toInteger] ⊤
have rw : Eq (α := Subalgebra ℤ (𝓞 K)) ℤ[hζ.toInteger]
  ℤ[((algebraMap (𝓞 ↥F₁) (𝓞 K) : (a : 𝓞 ↥F₁) → 𝓞 K) hζ₁_1.toInteger : 𝓞 K),
    ((algebraMap (𝓞 ↥F₂) (𝓞 K) : (a : 𝓞 ↥F₂) → 𝓞 K) hζ₂_1.toInteger : 𝓞 K)]
Tactic: rw [← IsDedekindDomain.adjoin_union_eq_top_of_isCoprime_differentialIdeal ℤ (𝓞 K) (𝓞 F₁)
    (𝓞 F₂) h_disj _ _ h₁ h₂, Set.image_singleton, Set.image_singleton, Set.singleton_union]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Basic (goal)
Goal:
K : Type u
inst : Field K
inst_1 : CharZero K
inst_2 : NumberField K
F₁ F₂ : IntermediateField ℚ K
n₁ n₂ : ℕ
inst_3 : NeZero n₁
inst_4 : NeZero n₂
inst_5 : IsCyclotomicExtension.{0, u} {n₁} ℚ ↥F₁
inst_6 : IsCyclotomicExtension.{0, u} {n₂} ℚ ↥F₂
ζ₁ : ↥F₁
hζ₁_1 : IsPrimitiveRoot ζ₁ n₁
h₁ : Eq (α := Subalgebra ℤ (𝓞 ↥F₁)) ℤ[hζ₁_1.toInteger] ⊤
ζ₂ : ↥F₂
hζ₂_1 : IsPrimitiveRoot ζ₂ n₂
h₂ : Eq (α := Subalgebra ℤ (𝓞 ↥F₂)) ℤ[hζ₂_1.toInteger] ⊤
h : n₁.Coprime n₂
htop : F₁ ⊔ F₂ = ⊤
ζ : K
hζ : IsPrimitiveRoot ζ (n₁ * n₂)
h_cpr : IsCoprime (NumberField.discr.{u} ↥F₁) (NumberField.discr.{u} ↥F₂)
h_disj : F₁.LinearDisjoint ↥F₂
hζ₁ : IsPrimitiveRoot (M := 𝓞 K) ((algebraMap (𝓞 ↥F₁) (𝓞 K) : (a : 𝓞 ↥F₁) → 𝓞 K) hζ₁_1.toInteger : 𝓞 K) n₁
hζ₂ : IsPrimitiveRoot (M := 𝓞 K) ((algebraMap (𝓞 ↥F₂) (𝓞 K) : (a : 𝓞 ↥F₂) → 𝓞 K) hζ₂_1.toInteger : 𝓞 K) n₂
rw :
  Eq (α := Subalgebra ℤ (𝓞 K)) ℤ[hζ.toInteger]
    ℤ[((algebraMap (𝓞 ↥F₁) (𝓞 K) : (a : 𝓞 ↥F₁) → 𝓞 K) hζ₁_1.toInteger : 𝓞 K),
      ((algebraMap (𝓞 ↥F₂) (𝓞 K) : (a : 𝓞 ↥F₂) → 𝓞 K) hζ₂_1.toInteger : 𝓞 K)]
⊢ Eq (α := Subalgebra ℤ (𝓞 K)) ℤ[hζ.toInteger] ⊤
have rw₁ : F₁.toSubalgebra ⊔ F₂.toSubalgebra = ⊤
Tactic: rw [← IsDedekindDomain.adjoin_union_eq_top_of_isCoprime_differentialIdeal ℤ (𝓞 K) (𝓞 F₁)
    (𝓞 F₂) h_disj _ _ h₁ h₂, Set.image_singleton, Set.image_singleton, Set.singleton_union]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Basic (goal)
Goal:
K : Type u
inst : Field K
inst_1 : CharZero K
inst_2 : NumberField K
F₁ F₂ : IntermediateField ℚ K
n₁ n₂ : ℕ
inst_3 : NeZero n₁
inst_4 : NeZero n₂
inst_5 : IsCyclotomicExtension.{0, u} {n₁} ℚ ↥F₁
inst_6 : IsCyclotomicExtension.{0, u} {n₂} ℚ ↥F₂
ζ₁ : ↥F₁
hζ₁_1 : IsPrimitiveRoot ζ₁ n₁
h₁ : Eq (α := Subalgebra ℤ (𝓞 ↥F₁)) ℤ[hζ₁_1.toInteger] ⊤
ζ₂ : ↥F₂
hζ₂_1 : IsPrimitiveRoot ζ₂ n₂
h₂ : Eq (α := Subalgebra ℤ (𝓞 ↥F₂)) ℤ[hζ₂_1.toInteger] ⊤
h : n₁.Coprime n₂
htop : F₁ ⊔ F₂ = ⊤
ζ : K
hζ : IsPrimitiveRoot ζ (n₁ * n₂)
h_cpr : IsCoprime (NumberField.discr.{u} ↥F₁) (NumberField.discr.{u} ↥F₂)
h_disj : F₁.LinearDisjoint ↥F₂
hζ₁ : IsPrimitiveRoot (M := 𝓞 K) ((algebraMap (𝓞 ↥F₁) (𝓞 K) : (a : 𝓞 ↥F₁) → 𝓞 K) hζ₁_1.toInteger : 𝓞 K) n₁
hζ₂ : IsPrimitiveRoot (M := 𝓞 K) ((algebraMap (𝓞 ↥F₂) (𝓞 K) : (a : 𝓞 ↥F₂) → 𝓞 K) hζ₂_1.toInteger : 𝓞 K) n₂
rw :
  Eq (α := Subalgebra ℤ (𝓞 K)) ℤ[hζ.toInteger]
    ℤ[((algebraMap (𝓞 ↥F₁) (𝓞 K) : (a : 𝓞 ↥F₁) → 𝓞 K) hζ₁_1.toInteger : 𝓞 K),
      ((algebraMap (𝓞 ↥F₂) (𝓞 K) : (a : 𝓞 ↥F₂) → 𝓞 K) hζ₂_1.toInteger : 𝓞 K)]
rw₁ : F₁.toSubalgebra ⊔ F₂.toSubalgebra = ⊤
⊢ Eq (α := Subalgebra ℤ (𝓞 K)) ℤ[hζ.toInteger] ⊤
have rw₂ : IsCoprime.{u} (R := Ideal (𝓞 K))
  (Ideal.map (R := 𝓞 ↥F₁) (F := 𝓞 ↥F₁ →+* 𝓞 K) (algebraMap (𝓞 ↥F₁) (𝓞 K)) (differentIdeal ℤ (𝓞 ↥F₁)))
  (Ideal.map (R := 𝓞 ↥F₂) (F := 𝓞 ↥F₂ →+* 𝓞 K) (algebraMap (𝓞 ↥F₂) (𝓞 K)) (differentIdeal ℤ (𝓞 ↥F₂)))
Tactic: rw [← IsDedekindDomain.adjoin_union_eq_top_of_isCoprime_differentialIdeal ℤ (𝓞 K) (𝓞 F₁)
    (𝓞 F₂) h_disj _ _ h₁ h₂, Set.image_singleton, Set.image_singleton, Set.singleton_union]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Basic (goal)
Goal:
K : Type u
inst : Field K
inst_1 : CharZero K
inst_2 : NumberField K
F₁ F₂ : IntermediateField ℚ K
n₁ n₂ : ℕ
inst_3 : NeZero n₁
inst_4 : NeZero n₂
inst_5 : IsCyclotomicExtension.{0, u} {n₁} ℚ ↥F₁
inst_6 : IsCyclotomicExtension.{0, u} {n₂} ℚ ↥F₂
ζ₁ : ↥F₁
hζ₁_1 : IsPrimitiveRoot ζ₁ n₁
h₁ : Eq (α := Subalgebra ℤ (𝓞 ↥F₁)) ℤ[hζ₁_1.toInteger] ⊤
ζ₂ : ↥F₂
hζ₂_1 : IsPrimitiveRoot ζ₂ n₂
h₂ : Eq (α := Subalgebra ℤ (𝓞 ↥F₂)) ℤ[hζ₂_1.toInteger] ⊤
h : n₁.Coprime n₂
htop : F₁ ⊔ F₂ = ⊤
ζ : K
hζ : IsPrimitiveRoot ζ (n₁ * n₂)
h_cpr : IsCoprime (NumberField.discr.{u} ↥F₁) (NumberField.discr.{u} ↥F₂)
h_disj : F₁.LinearDisjoint ↥F₂
hζ₁ : IsPrimitiveRoot (M := 𝓞 K) ((algebraMap (𝓞 ↥F₁) (𝓞 K) : (a : 𝓞 ↥F₁) → 𝓞 K) hζ₁_1.toInteger : 𝓞 K) n₁
hζ₂ : IsPrimitiveRoot (M := 𝓞 K) ((algebraMap (𝓞 ↥F₂) (𝓞 K) : (a : 𝓞 ↥F₂) → 𝓞 K) hζ₂_1.toInteger : 𝓞 K) n₂
⊢ Eq (α := Subalgebra ℤ (𝓞 K)) ℤ[hζ.toInteger]
    ℤ[((algebraMap (𝓞 ↥F₁) (𝓞 K) : (a : 𝓞 ↥F₁) → 𝓞 K) hζ₁_1.toInteger : 𝓞 K),
      ((algebraMap (𝓞 ↥F₂) (𝓞 K) : (a : 𝓞 ↥F₂) → 𝓞 K) hζ₂_1.toInteger : 𝓞 K)]
have refine : IsPrimitiveRoot hζ.toInteger (n₁.lcm n₂)
Tactic: refine (IsPrimitiveRoot.adjoin_pair_eq ℤ hζ₁ hζ₂ (NeZero.ne _) (NeZero.ne _) ?_).symm
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Basic (goal)
Goal:
K : Type u
inst : Field K
inst_1 : CharZero K
inst_2 : NumberField K
F₁ F₂ : IntermediateField ℚ K
n₁ n₂ : ℕ
inst_3 : NeZero n₁
inst_4 : NeZero n₂
inst_5 : IsCyclotomicExtension.{0, u} {n₁} ℚ ↥F₁
inst_6 : IsCyclotomicExtension.{0, u} {n₂} ℚ ↥F₂
ζ₁ : ↥F₁
hζ₁_1 : IsPrimitiveRoot ζ₁ n₁
h₁ : Eq (α := Subalgebra ℤ (𝓞 ↥F₁)) ℤ[hζ₁_1.toInteger] ⊤
ζ₂ : ↥F₂
hζ₂_1 : IsPrimitiveRoot ζ₂ n₂
h₂ : Eq (α := Subalgebra ℤ (𝓞 ↥F₂)) ℤ[hζ₂_1.toInteger] ⊤
h : n₁.Coprime n₂
htop : F₁ ⊔ F₂ = ⊤
ζ : K
hζ : IsPrimitiveRoot ζ (n₁ * n₂)
h_cpr : IsCoprime (NumberField.discr.{u} ↥F₁) (NumberField.discr.{u} ↥F₂)
h_disj : F₁.LinearDisjoint ↥F₂
hζ₁ : IsPrimitiveRoot (M := 𝓞 K) ((algebraMap (𝓞 ↥F₁) (𝓞 K) : (a : 𝓞 ↥F₁) → 𝓞 K) hζ₁_1.toInteger : 𝓞 K) n₁
hζ₂ : IsPrimitiveRoot (M := 𝓞 K) ((algebraMap (𝓞 ↥F₂) (𝓞 K) : (a : 𝓞 ↥F₂) → 𝓞 K) hζ₂_1.toInteger : 𝓞 K) n₂
⊢ IsPrimitiveRoot hζ.toInteger (n₁.lcm n₂)
have rw : IsPrimitiveRoot hζ.toInteger (n₁ * n₂)
Tactic: rw [Nat.Coprime.lcm_eq_mul h]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Basic (hypothesis)
Goal:
n : ℕ
K : Type u
inst : Field K
inst_1 : CharZero K
hn : NeZero n
hK : IsCyclotomicExtension {n} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ n
⊢ Eq (α := Subalgebra ℤ (𝓞 K)) ℤ[hζ.toInteger] ⊤
have this : NumberField K
Tactic: haveI : NumberField K := IsCyclotomicExtension.numberField {n} ℚ K
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Basic (hypothesis)
Goal:
p k : ℕ
hp : Nat.Prime p
K : Type u
inst : Field K
inst_1 : CharZero K
hn : NeZero (p ^ k)
hK : IsCyclotomicExtension {p ^ k} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ (p ^ k)
this : NumberField K
⊢ Eq (α := Subalgebra ℤ (𝓞 K)) ℤ[hζ.toInteger] ⊤
have this₁ : Fact (Nat.Prime p)
Tactic: have : Fact (p.Prime) := ⟨hp⟩
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Basic (goal)
Goal:
p k : ℕ
hp : Nat.Prime p
K : Type u
inst : Field K
inst_1 : CharZero K
hn : NeZero (p ^ k)
hK : IsCyclotomicExtension {p ^ k} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ (p ^ k)
this_1 : NumberField K
this : Fact (Nat.Prime p)
⊢ Eq (α := Subalgebra ℤ (𝓞 K)) ℤ[hζ.toInteger] ⊤
have prime_pow : Eq (α := Subalgebra ℤ (𝓞 K)) ℤ[hζ.toInteger] ℤ[hζ.integralPowerBasisOfPrimePow.gen]
Tactic: rw [← hζ.integralPowerBasisOfPrimePow.adjoin_gen_eq_top, hζ.integralPowerBasisOfPrimePow_gen]