internlm/Lean-Github huggingface dataset:
Theorem: contains_two_primitive_roots
Proof state before:
case inr.inr
p✝ : ℕ+
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p✝
inst✝¹ : NumberField K
p q : ℕ
x y : K
inst✝ : FiniteDimensional ℚ K
hx : IsPrimitiveRoot x p
hy : IsPrimitiveRoot y q
hppos : p > 0
hqpos : q > 0
⊢ (lcm p q).totient ≤ FiniteDimensional.finrank ℚ K
Tactic:
let k := lcm p q
Proof state after:
case inr.inr
p✝ : ℕ+
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p✝
inst✝¹ : NumberField K
p q : ℕ
x y : K
inst✝ : FiniteDimensional ℚ K
hx : IsPrimitiveRoot x p
hy : IsPrimitiveRoot y q
hppos : p > 0
hqpos : q > 0
k : ℕ := lcm p q
⊢ (lcm p q).totient ≤ FiniteDimensional.finrank ℚ K
Theorem: contains_two_primitive_roots
Proof state before:
case inr.inr
p✝ : ℕ+
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p✝
inst✝¹ : NumberField K
p q : ℕ
x y : K
inst✝ : FiniteDimensional ℚ K
hx : IsPrimitiveRoot x p
hy : IsPrimitiveRoot y q
hppos : p > 0
hqpos : q > 0
k : ℕ := lcm p q
⊢ (lcm p q).totient ≤ FiniteDimensional.finrank ℚ K
Tactic:
have hkpos : 0 < k := Nat.pos_of_ne_zero (Nat.lcm_ne_zero hppos.ne' hqpos.ne')
Proof state after:
case inr.inr
p✝ : ℕ+
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p✝
inst✝¹ : NumberField K
p q : ℕ
x y : K
inst✝ : FiniteDimensional ℚ K
hx : IsPrimitiveRoot x p
hy : IsPrimitiveRoot y q
hppos : p > 0
hqpos : q > 0
k : ℕ := lcm p q
hkpos : 0 < k
⊢ (lcm p q).totient ≤ FiniteDimensional.finrank ℚ K
Theorem: contains_two_primitive_roots
Proof state before:
case inr.inr
p✝ : ℕ+
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p✝
inst✝¹ : NumberField K
p q : ℕ
x y : K
inst✝ : FiniteDimensional ℚ K
hx : IsPrimitiveRoot x p
hy : IsPrimitiveRoot y q
hppos : p > 0
hqpos : q > 0
k : ℕ := lcm p q
hkpos : 0 < k
⊢ (lcm p q).totient ≤ FiniteDimensional.finrank ℚ K
Tactic:
let xu := IsUnit.unit (hx.isUnit hppos)
Proof state after:
case inr.inr
p✝ : ℕ+
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p✝
inst✝¹ : NumberField K
p q : ℕ
x y : K
inst✝ : FiniteDimensional ℚ K
hx : IsPrimitiveRoot x p
hy : IsPrimitiveRoot y q
hppos : p > 0
hqpos : q > 0
k : ℕ := lcm p q
hkpos : 0 < k
xu : Kˣ := ⋯.unit
⊢ (lcm p q).totient ≤ FiniteDimensional.finrank ℚ K
Theorem: contains_two_primitive_roots
Proof state before:
case inr.inr
p✝ : ℕ+
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p✝
inst✝¹ : NumberField K
p q : ℕ
x y : K
inst✝ : FiniteDimensional ℚ K
hx : IsPrimitiveRoot x p
hy : IsPrimitiveRoot y q
hppos : p > 0
hqpos : q > 0
k : ℕ := lcm p q
hkpos : 0 < k
xu : Kˣ := ⋯.unit
⊢ (lcm p q).totient ≤ FiniteDimensional.finrank ℚ K
Tactic:
let yu := IsUnit.unit (hy.isUnit hqpos)
Proof state after:
case inr.inr
p✝ : ℕ+
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p✝
inst✝¹ : NumberField K
p q : ℕ
x y : K
inst✝ : FiniteDimensional ℚ K
hx : IsPrimitiveRoot x p
hy : IsPrimitiveRoot y q
hppos : p > 0
hqpos : q > 0
k : ℕ := lcm p q
hkpos : 0 < k
xu : Kˣ := ⋯.unit
yu : Kˣ := ⋯.unit
⊢ (lcm p q).totient ≤ FiniteDimensional.finrank ℚ K
Theorem: contains_two_primitive_roots
Proof state before:
case inr.inr
p✝ : ℕ+
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p✝
inst✝¹ : NumberField K
p q : ℕ
x y : K
inst✝ : FiniteDimensional ℚ K
hx : IsPrimitiveRoot x p
hy : IsPrimitiveRoot y q
hppos : p > 0
hqpos : q > 0
k : ℕ := lcm p q
hkpos : 0 < k
xu : Kˣ := ⋯.unit
yu : Kˣ := ⋯.unit
⊢ (lcm p q).totient ≤ FiniteDimensional.finrank ℚ K
Tactic:
have hxmem : xu ∈ rootsOfUnity ⟨k, hkpos⟩ K :=  by
  rw [mem_rootsOfUnity, PNat.mk_coe, ← Units.val_eq_one, Units.val_pow_eq_pow_val,
    IsUnit.unit_spec]
  exact (hx.pow_eq_one_iff_dvd _).2 (dvd_lcm_left _ _)
Proof state after:
case inr.inr
p✝ : ℕ+
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p✝
inst✝¹ : NumberField K
p q : ℕ
x y : K
inst✝ : FiniteDimensional ℚ K
hx : IsPrimitiveRoot x p
hy : IsPrimitiveRoot y q
hppos : p > 0
hqpos : q > 0
k : ℕ := lcm p q
hkpos : 0 < k
xu : Kˣ := ⋯.unit
yu : Kˣ := ⋯.unit
hxmem : xu ∈ rootsOfUnity ⟨k, hkpos⟩ K
⊢ (lcm p q).totient ≤ FiniteDimensional.finrank ℚ K
Theorem: contains_two_primitive_roots
Proof state before:
case inr.inr
p✝ : ℕ+
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p✝
inst✝¹ : NumberField K
p q : ℕ
x y : K
inst✝ : FiniteDimensional ℚ K
hx : IsPrimitiveRoot x p
hy : IsPrimitiveRoot y q
hppos : p > 0
hqpos : q > 0
k : ℕ := lcm p q
hkpos : 0 < k
xu : Kˣ := ⋯.unit
yu : Kˣ := ⋯.unit
hxmem : xu ∈ rootsOfUnity ⟨k, hkpos⟩ K
⊢ (lcm p q).totient ≤ FiniteDimensional.finrank ℚ K
Tactic:
have hymem : yu ∈ rootsOfUnity ⟨k, hkpos⟩ K := by
  rw [mem_rootsOfUnity, PNat.mk_coe, ← Units.val_eq_one, Units.val_pow_eq_pow_val,
    IsUnit.unit_spec]
  exact (hy.pow_eq_one_iff_dvd _).2 (dvd_lcm_right _ _)
Proof state after:
case inr.inr
p✝ : ℕ+
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p✝
inst✝¹ : NumberField K
p q : ℕ
x y : K
inst✝ : FiniteDimensional ℚ K
hx : IsPrimitiveRoot x p
hy : IsPrimitiveRoot y q
hppos : p > 0
hqpos : q > 0
k : ℕ := lcm p q
hkpos : 0 < k
xu : Kˣ := ⋯.unit
yu : Kˣ := ⋯.unit
hxmem : xu ∈ rootsOfUnity ⟨k, hkpos⟩ K
hymem : yu ∈ rootsOfUnity ⟨k, hkpos⟩ K
⊢ (lcm p q).totient ≤ FiniteDimensional.finrank ℚ K
Theorem: contains_two_primitive_roots
Proof state before:
case inr.inr
p✝ : ℕ+
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p✝
inst✝¹ : NumberField K
p q : ℕ
x y : K
inst✝ : FiniteDimensional ℚ K
hx : IsPrimitiveRoot x p
hy : IsPrimitiveRoot y q
hppos : p > 0
hqpos : q > 0
k : ℕ := lcm p q
hkpos : 0 < k
xu : Kˣ := ⋯.unit
yu : Kˣ := ⋯.unit
hxmem : xu ∈ rootsOfUnity ⟨k, hkpos⟩ K
hymem : yu ∈ rootsOfUnity ⟨k, hkpos⟩ K
⊢ (lcm p q).totient ≤ FiniteDimensional.finrank ℚ K
Tactic:
have hxuord : orderOf (⟨xu, hxmem⟩ : rootsOfUnity ⟨k, hkpos⟩ K) = p := by
  rw [← orderOf_injective (rootsOfUnity ⟨k, hkpos⟩ K).subtype Subtype.coe_injective,
    Subgroup.coeSubtype, Subgroup.coe_mk, ← orderOf_units, IsUnit.unit_spec]
  exact hx.eq_orderOf.symm
Proof state after:
case inr.inr
p✝ : ℕ+
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p✝
inst✝¹ : NumberField K
p q : ℕ
x y : K
inst✝ : FiniteDimensional ℚ K
hx : IsPrimitiveRoot x p
hy : IsPrimitiveRoot y q
hppos : p > 0
hqpos : q > 0
k : ℕ := lcm p q
hkpos : 0 < k
xu : Kˣ := ⋯.unit
yu : Kˣ := ⋯.unit
hxmem : xu ∈ rootsOfUnity ⟨k, hkpos⟩ K
hymem : yu ∈ rootsOfUnity ⟨k, hkpos⟩ K
hxuord : orderOf ⟨xu, hxmem⟩ = p
⊢ (lcm p q).totient ≤ FiniteDimensional.finrank ℚ K
Theorem: contains_two_primitive_roots
Proof state before:
case inr.inr
p✝ : ℕ+
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p✝
inst✝¹ : NumberField K
p q : ℕ
x y : K
inst✝ : FiniteDimensional ℚ K
hx : IsPrimitiveRoot x p
hy : IsPrimitiveRoot y q
hppos : p > 0
hqpos : q > 0
k : ℕ := lcm p q
hkpos : 0 < k
xu : Kˣ := ⋯.unit
yu : Kˣ := ⋯.unit
hxmem : xu ∈ rootsOfUnity ⟨k, hkpos⟩ K
hymem : yu ∈ rootsOfUnity ⟨k, hkpos⟩ K
hxuord : orderOf ⟨xu, hxmem⟩ = p
⊢ (lcm p q).totient ≤ FiniteDimensional.finrank ℚ K
Tactic:
have hyuord : orderOf (⟨yu, hymem⟩ : rootsOfUnity ⟨k, hkpos⟩ K) = q := by
  rw [← orderOf_injective (rootsOfUnity ⟨k, hkpos⟩ K).subtype Subtype.coe_injective,
    Subgroup.coeSubtype, Subgroup.coe_mk, ← orderOf_units, IsUnit.unit_spec]
  exact hy.eq_orderOf.symm
Proof state after:
case inr.inr
p✝ : ℕ+
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p✝
inst✝¹ : NumberField K
p q : ℕ
x y : K
inst✝ : FiniteDimensional ℚ K
hx : IsPrimitiveRoot x p
hy : IsPrimitiveRoot y q
hppos : p > 0
hqpos : q > 0
k : ℕ := lcm p q
hkpos : 0 < k
xu : Kˣ := ⋯.unit
yu : Kˣ := ⋯.unit
hxmem : xu ∈ rootsOfUnity ⟨k, hkpos⟩ K
hymem : yu ∈ rootsOfUnity ⟨k, hkpos⟩ K
hxuord : orderOf ⟨xu, hxmem⟩ = p
hyuord : orderOf ⟨yu, hymem⟩ = q
⊢ (lcm p q).totient ≤ FiniteDimensional.finrank ℚ K
Theorem: contains_two_primitive_roots
Proof state before:
case inr.inr
p✝ : ℕ+
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p✝
inst✝¹ : NumberField K
p q : ℕ
x y : K
inst✝ : FiniteDimensional ℚ K
hx : IsPrimitiveRoot x p
hy : IsPrimitiveRoot y q
hppos : p > 0
hqpos : q > 0
k : ℕ := lcm p q
hkpos : 0 < k
xu : Kˣ := ⋯.unit
yu : Kˣ := ⋯.unit
hxmem : xu ∈ rootsOfUnity ⟨k, hkpos⟩ K
hymem : yu ∈ rootsOfUnity ⟨k, hkpos⟩ K
hxuord : orderOf ⟨xu, hxmem⟩ = p
hyuord : orderOf ⟨yu, hymem⟩ = q
⊢ (lcm p q).totient ≤ FiniteDimensional.finrank ℚ K
Tactic:
obtain ⟨g : rootsOfUnity ⟨k, hkpos⟩ K, hg⟩ :=
  IsCyclic.exists_monoid_generator (α := rootsOfUnity ⟨k, hkpos⟩ K)
Proof state after:
case inr.inr.intro
p✝ : ℕ+
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p✝
inst✝¹ : NumberField K
p q : ℕ
x y : K
inst✝ : FiniteDimensional ℚ K
hx : IsPrimitiveRoot x p
hy : IsPrimitiveRoot y q
hppos : p > 0
hqpos : q > 0
k : ℕ := lcm p q
hkpos : 0 < k
xu : Kˣ := ⋯.unit
yu : Kˣ := ⋯.unit
hxmem : xu ∈ rootsOfUnity ⟨k, hkpos⟩ K
hymem : yu ∈ rootsOfUnity ⟨k, hkpos⟩ K
hxuord : orderOf ⟨xu, hxmem⟩ = p
hyuord : orderOf ⟨yu, hymem⟩ = q
g : ↥(rootsOfUnity ⟨k, hkpos⟩ K)
hg : ∀ (y : ↥(rootsOfUnity ⟨k, hkpos⟩ K)), y ∈ Submonoid.powers g
⊢ (lcm p q).totient ≤ FiniteDimensional.finrank ℚ K
Theorem: contains_two_primitive_roots
Proof state before:
case inr.inr.intro
p✝ : ℕ+
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p✝
inst✝¹ : NumberField K
p q : ℕ
x y : K
inst✝ : FiniteDimensional ℚ K
hx : IsPrimitiveRoot x p
hy : IsPrimitiveRoot y q
hppos : p > 0
hqpos : q > 0
k : ℕ := lcm p q
hkpos : 0 < k
xu : Kˣ := ⋯.unit
yu : Kˣ := ⋯.unit
hxmem : xu ∈ rootsOfUnity ⟨k, hkpos⟩ K
hymem : yu ∈ rootsOfUnity ⟨k, hkpos⟩ K
hxuord : orderOf ⟨xu, hxmem⟩ = p
hyuord : orderOf ⟨yu, hymem⟩ = q
g : ↥(rootsOfUnity ⟨k, hkpos⟩ K)
hg : ∀ (y : ↥(rootsOfUnity ⟨k, hkpos⟩ K)), y ∈ Submonoid.powers g
⊢ (lcm p q).totient ≤ FiniteDimensional.finrank ℚ K
Tactic:
obtain ⟨nx, hnx⟩ := hg ⟨xu, hxmem⟩
Proof state after:
case inr.inr.intro.intro
p✝ : ℕ+
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p✝
inst✝¹ : NumberField K
p q : ℕ
x y : K
inst✝ : FiniteDimensional ℚ K
hx : IsPrimitiveRoot x p
hy : IsPrimitiveRoot y q
hppos : p > 0
hqpos : q > 0
k : ℕ := lcm p q
hkpos : 0 < k
xu : Kˣ := ⋯.unit
yu : Kˣ := ⋯.unit
hxmem : xu ∈ rootsOfUnity ⟨k, hkpos⟩ K
hymem : yu ∈ rootsOfUnity ⟨k, hkpos⟩ K
hxuord : orderOf ⟨xu, hxmem⟩ = p
hyuord : orderOf ⟨yu, hymem⟩ = q
g : ↥(rootsOfUnity ⟨k, hkpos⟩ K)
hg : ∀ (y : ↥(rootsOfUnity ⟨k, hkpos⟩ K)), y ∈ Submonoid.powers g
nx : ℕ
hnx : (fun x => g ^ x) nx = ⟨xu, hxmem⟩
⊢ (lcm p q).totient ≤ FiniteDimensional.finrank ℚ K
Theorem: contains_two_primitive_roots
Proof state before:
case inr.inr.intro.intro
p✝ : ℕ+
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p✝
inst✝¹ : NumberField K
p q : ℕ
x y : K
inst✝ : FiniteDimensional ℚ K
hx : IsPrimitiveRoot x p
hy : IsPrimitiveRoot y q
hppos : p > 0
hqpos : q > 0
k : ℕ := lcm p q
hkpos : 0 < k
xu : Kˣ := ⋯.unit
yu : Kˣ := ⋯.unit
hxmem : xu ∈ rootsOfUnity ⟨k, hkpos⟩ K
hymem : yu ∈ rootsOfUnity ⟨k, hkpos⟩ K
hxuord : orderOf ⟨xu, hxmem⟩ = p
hyuord : orderOf ⟨yu, hymem⟩ = q
g : ↥(rootsOfUnity ⟨k, hkpos⟩ K)
hg : ∀ (y : ↥(rootsOfUnity ⟨k, hkpos⟩ K)), y ∈ Submonoid.powers g
nx : ℕ
hnx : (fun x => g ^ x) nx = ⟨xu, hxmem⟩
⊢ (lcm p q).totient ≤ FiniteDimensional.finrank ℚ K
Tactic:
obtain ⟨ny, hny⟩ := hg ⟨yu, hymem⟩
Proof state after:
case inr.inr.intro.intro.intro
p✝ : ℕ+
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p✝
inst✝¹ : NumberField K
p q : ℕ
x y : K
inst✝ : FiniteDimensional ℚ K
hx : IsPrimitiveRoot x p
hy : IsPrimitiveRoot y q
hppos : p > 0
hqpos : q > 0
k : ℕ := lcm p q
hkpos : 0 < k
xu : Kˣ := ⋯.unit
yu : Kˣ := ⋯.unit
hxmem : xu ∈ rootsOfUnity ⟨k, hkpos⟩ K
hymem : yu ∈ rootsOfUnity ⟨k, hkpos⟩ K
hxuord : orderOf ⟨xu, hxmem⟩ = p
hyuord : orderOf ⟨yu, hymem⟩ = q
g : ↥(rootsOfUnity ⟨k, hkpos⟩ K)
hg : ∀ (y : ↥(rootsOfUnity ⟨k, hkpos⟩ K)), y ∈ Submonoid.powers g
nx : ℕ
hnx : (fun x => g ^ x) nx = ⟨xu, hxmem⟩
ny : ℕ
hny : (fun x => g ^ x) ny = ⟨yu, hymem⟩
⊢ (lcm p q).totient ≤ FiniteDimensional.finrank ℚ K
Theorem: contains_two_primitive_roots
Proof state before:
case inr.inr.intro.intro.intro
p✝ : ℕ+
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p✝
inst✝¹ : NumberField K
p q : ℕ
x y : K
inst✝ : FiniteDimensional ℚ K
hx : IsPrimitiveRoot x p
hy : IsPrimitiveRoot y q
hppos : p > 0
hqpos : q > 0
k : ℕ := lcm p q
hkpos : 0 < k
xu : Kˣ := ⋯.unit
yu : Kˣ := ⋯.unit
hxmem : xu ∈ rootsOfUnity ⟨k, hkpos⟩ K
hymem : yu ∈ rootsOfUnity ⟨k, hkpos⟩ K
hxuord : orderOf ⟨xu, hxmem⟩ = p
hyuord : orderOf ⟨yu, hymem⟩ = q
g : ↥(rootsOfUnity ⟨k, hkpos⟩ K)
hg : ∀ (y : ↥(rootsOfUnity ⟨k, hkpos⟩ K)), y ∈ Submonoid.powers g
nx : ℕ
hnx : (fun x => g ^ x) nx = ⟨xu, hxmem⟩
ny : ℕ
hny : (fun x => g ^ x) ny = ⟨yu, hymem⟩
H : orderOf g = k
⊢ (lcm p q).totient ≤ FiniteDimensional.finrank ℚ K
Tactic:
have hroot := IsPrimitiveRoot.orderOf g
Proof state after:
case inr.inr.intro.intro.intro
p✝ : ℕ+
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p✝
inst✝¹ : NumberField K
p q : ℕ
x y : K
inst✝ : FiniteDimensional ℚ K
hx : IsPrimitiveRoot x p
hy : IsPrimitiveRoot y q
hppos : p > 0
hqpos : q > 0
k : ℕ := lcm p q
hkpos : 0 < k
xu : Kˣ := ⋯.unit
yu : Kˣ := ⋯.unit
hxmem : xu ∈ rootsOfUnity ⟨k, hkpos⟩ K
hymem : yu ∈ rootsOfUnity ⟨k, hkpos⟩ K
hxuord : orderOf ⟨xu, hxmem⟩ = p
hyuord : orderOf ⟨yu, hymem⟩ = q
g : ↥(rootsOfUnity ⟨k, hkpos⟩ K)
hg : ∀ (y : ↥(rootsOfUnity ⟨k, hkpos⟩ K)), y ∈ Submonoid.powers g
nx : ℕ
hnx : (fun x => g ^ x) nx = ⟨xu, hxmem⟩
ny : ℕ
hny : (fun x => g ^ x) ny = ⟨yu, hymem⟩
H : orderOf g = k
hroot : IsPrimitiveRoot g (orderOf g)
⊢ (lcm p q).totient ≤ FiniteDimensional.finrank ℚ K
Theorem: contains_two_primitive_roots
Proof state before:
case inr.inr.intro.intro.intro
p✝ : ℕ+
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p✝
inst✝¹ : NumberField K
p q : ℕ
x y : K
inst✝ : FiniteDimensional ℚ K
hx : IsPrimitiveRoot x p
hy : IsPrimitiveRoot y q
hppos : p > 0
hqpos : q > 0
k : ℕ := lcm p q
hkpos : 0 < k
xu : Kˣ := ⋯.unit
yu : Kˣ := ⋯.unit
hxmem : xu ∈ rootsOfUnity ⟨k, hkpos⟩ K
hymem : yu ∈ rootsOfUnity ⟨k, hkpos⟩ K
hxuord : orderOf ⟨xu, hxmem⟩ = p
hyuord : orderOf ⟨yu, hymem⟩ = q
g : ↥(rootsOfUnity ⟨k, hkpos⟩ K)
hg : ∀ (y : ↥(rootsOfUnity ⟨k, hkpos⟩ K)), y ∈ Submonoid.powers g
nx : ℕ
hnx : (fun x => g ^ x) nx = ⟨xu, hxmem⟩
ny : ℕ
hny : (fun x => g ^ x) ny = ⟨yu, hymem⟩
H : orderOf g = k
hroot : IsPrimitiveRoot g (orderOf g)
⊢ (lcm p q).totient ≤ FiniteDimensional.finrank ℚ K
Tactic:
rw [H, ← IsPrimitiveRoot.coe_submonoidClass_iff, ← IsPrimitiveRoot.coe_units_iff] at hroot
Proof state after:
case inr.inr.intro.intro.intro
p✝ : ℕ+
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p✝
inst✝¹ : NumberField K
p q : ℕ
x y : K
inst✝ : FiniteDimensional ℚ K
hx : IsPrimitiveRoot x p
hy : IsPrimitiveRoot y q
hppos : p > 0
hqpos : q > 0
k : ℕ := lcm p q
hkpos : 0 < k
xu : Kˣ := ⋯.unit
yu : Kˣ := ⋯.unit
hxmem : xu ∈ rootsOfUnity ⟨k, hkpos⟩ K
hymem : yu ∈ rootsOfUnity ⟨k, hkpos⟩ K
hxuord : orderOf ⟨xu, hxmem⟩ = p
hyuord : orderOf ⟨yu, hymem⟩ = q
g : ↥(rootsOfUnity ⟨k, hkpos⟩ K)
hg : ∀ (y : ↥(rootsOfUnity ⟨k, hkpos⟩ K)), y ∈ Submonoid.powers g
nx : ℕ
hnx : (fun x => g ^ x) nx = ⟨xu, hxmem⟩
ny : ℕ
hny : (fun x => g ^ x) ny = ⟨yu, hymem⟩
H : orderOf g = k
hroot : IsPrimitiveRoot (↑↑g) k
⊢ (lcm p q).totient ≤ FiniteDimensional.finrank ℚ K
Theorem: contains_two_primitive_roots
Proof state before:
case inr.inr.intro.intro.intro
p✝ : ℕ+
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p✝
inst✝¹ : NumberField K
p q : ℕ
x y : K
inst✝ : FiniteDimensional ℚ K
hx : IsPrimitiveRoot x p
hy : IsPrimitiveRoot y q
hppos : p > 0
hqpos : q > 0
k : ℕ := lcm p q
hkpos : 0 < k
xu : Kˣ := ⋯.unit
yu : Kˣ := ⋯.unit
hxmem : xu ∈ rootsOfUnity ⟨k, hkpos⟩ K
hymem : yu ∈ rootsOfUnity ⟨k, hkpos⟩ K
hxuord : orderOf ⟨xu, hxmem⟩ = p
hyuord : orderOf ⟨yu, hymem⟩ = q
g : ↥(rootsOfUnity ⟨k, hkpos⟩ K)
hg : ∀ (y : ↥(rootsOfUnity ⟨k, hkpos⟩ K)), y ∈ Submonoid.powers g
nx : ℕ
hnx : (fun x => g ^ x) nx = ⟨xu, hxmem⟩
ny : ℕ
hny : (fun x => g ^ x) ny = ⟨yu, hymem⟩
H : orderOf g = k
hroot : IsPrimitiveRoot (↑↑g) k
⊢ (lcm p q).totient ≤ FiniteDimensional.finrank ℚ K
Tactic:
conv at hroot =>
  congr
  rfl
  rw [show k = (⟨k, hkpos⟩ : ℕ+) by simp]
Proof state after:
case inr.inr.intro.intro.intro
p✝ : ℕ+
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p✝
inst✝¹ : NumberField K
p q : ℕ
x y : K
inst✝ : FiniteDimensional ℚ K
hx : IsPrimitiveRoot x p
hy : IsPrimitiveRoot y q
hppos : p > 0
hqpos : q > 0
k : ℕ := lcm p q
hkpos : 0 < k
xu : Kˣ := ⋯.unit
yu : Kˣ := ⋯.unit
hxmem : xu ∈ rootsOfUnity ⟨k, hkpos⟩ K
hymem : yu ∈ rootsOfUnity ⟨k, hkpos⟩ K
hxuord : orderOf ⟨xu, hxmem⟩ = p
hyuord : orderOf ⟨yu, hymem⟩ = q
g : ↥(rootsOfUnity ⟨k, hkpos⟩ K)
hg : ∀ (y : ↥(rootsOfUnity ⟨k, hkpos⟩ K)), y ∈ Submonoid.powers g
nx : ℕ
hnx : (fun x => g ^ x) nx = ⟨xu, hxmem⟩
ny : ℕ
hny : (fun x => g ^ x) ny = ⟨yu, hymem⟩
H : orderOf g = k
hroot : IsPrimitiveRoot ↑↑g ↑⟨k, hkpos⟩
⊢ (lcm p q).totient ≤ FiniteDimensional.finrank ℚ K
Theorem: contains_two_primitive_roots
Proof state before:
case inr.inr.intro.intro.intro
p✝ : ℕ+
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p✝
inst✝¹ : NumberField K
p q : ℕ
x y : K
inst✝ : FiniteDimensional ℚ K
hx : IsPrimitiveRoot x p
hy : IsPrimitiveRoot y q
hppos : p > 0
hqpos : q > 0
k : ℕ := lcm p q
hkpos : 0 < k
xu : Kˣ := ⋯.unit
yu : Kˣ := ⋯.unit
hxmem : xu ∈ rootsOfUnity ⟨k, hkpos⟩ K
hymem : yu ∈ rootsOfUnity ⟨k, hkpos⟩ K
hxuord : orderOf ⟨xu, hxmem⟩ = p
hyuord : orderOf ⟨yu, hymem⟩ = q
g : ↥(rootsOfUnity ⟨k, hkpos⟩ K)
hg : ∀ (y : ↥(rootsOfUnity ⟨k, hkpos⟩ K)), y ∈ Submonoid.powers g
nx : ℕ
hnx : (fun x => g ^ x) nx = ⟨xu, hxmem⟩
ny : ℕ
hny : (fun x => g ^ x) ny = ⟨yu, hymem⟩
H : orderOf g = k
hroot : IsPrimitiveRoot ↑↑g ↑⟨k, hkpos⟩
⊢ (lcm p q).totient ≤ FiniteDimensional.finrank ℚ K
Tactic:
haveI := IsPrimitiveRoot.adjoin_isCyclotomicExtension ℚ hroot
Proof state after:
case inr.inr.intro.intro.intro
p✝ : ℕ+
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p✝
inst✝¹ : NumberField K
p q : ℕ
x y : K
inst✝ : FiniteDimensional ℚ K
hx : IsPrimitiveRoot x p
hy : IsPrimitiveRoot y q
hppos : p > 0
hqpos : q > 0
k : ℕ := lcm p q
hkpos : 0 < k
xu : Kˣ := ⋯.unit
yu : Kˣ := ⋯.unit
hxmem : xu ∈ rootsOfUnity ⟨k, hkpos⟩ K
hymem : yu ∈ rootsOfUnity ⟨k, hkpos⟩ K
hxuord : orderOf ⟨xu, hxmem⟩ = p
hyuord : orderOf ⟨yu, hymem⟩ = q
g : ↥(rootsOfUnity ⟨k, hkpos⟩ K)
hg : ∀ (y : ↥(rootsOfUnity ⟨k, hkpos⟩ K)), y ∈ Submonoid.powers g
nx : ℕ
hnx : (fun x => g ^ x) nx = ⟨xu, hxmem⟩
ny : ℕ
hny : (fun x => g ^ x) ny = ⟨yu, hymem⟩
H : orderOf g = k
hroot : IsPrimitiveRoot ↑↑g ↑⟨k, hkpos⟩
this : IsCyclotomicExtension {⟨k, hkpos⟩} ℚ ↥(Algebra.adjoin ℚ {↑↑g})
⊢ (lcm p q).totient ≤ FiniteDimensional.finrank ℚ K
Theorem: contains_two_primitive_roots
Proof state before:
case inr.inr.intro.intro.intro
p✝ : ℕ+
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p✝
inst✝¹ : NumberField K
p q : ℕ
x y : K
inst✝ : FiniteDimensional ℚ K
hx : IsPrimitiveRoot x p
hy : IsPrimitiveRoot y q
hppos : p > 0
hqpos : q > 0
k : ℕ := lcm p q
hkpos : 0 < k
xu : Kˣ := ⋯.unit
yu : Kˣ := ⋯.unit
hxmem : xu ∈ rootsOfUnity ⟨k, hkpos⟩ K
hymem : yu ∈ rootsOfUnity ⟨k, hkpos⟩ K
hxuord : orderOf ⟨xu, hxmem⟩ = p
hyuord : orderOf ⟨yu, hymem⟩ = q
g : ↥(rootsOfUnity ⟨k, hkpos⟩ K)
hg : ∀ (y : ↥(rootsOfUnity ⟨k, hkpos⟩ K)), y ∈ Submonoid.powers g
nx : ℕ
hnx : (fun x => g ^ x) nx = ⟨xu, hxmem⟩
ny : ℕ
hny : (fun x => g ^ x) ny = ⟨yu, hymem⟩
H : orderOf g = k
hroot : IsPrimitiveRoot ↑↑g ↑⟨k, hkpos⟩
this : IsCyclotomicExtension {⟨k, hkpos⟩} ℚ ↥(Algebra.adjoin ℚ {↑↑g})
⊢ (lcm p q).totient ≤ FiniteDimensional.finrank ℚ K
Tactic:
convert Submodule.finrank_le (Subalgebra.toSubmodule (Algebra.adjoin ℚ ({g.1.1} : Set K)))
Proof state after:
case h.e'_3
p✝ : ℕ+
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p✝
inst✝¹ : NumberField K
p q : ℕ
x y : K
inst✝ : FiniteDimensional ℚ K
hx : IsPrimitiveRoot x p
hy : IsPrimitiveRoot y q
hppos : p > 0
hqpos : q > 0
k : ℕ := lcm p q
hkpos : 0 < k
xu : Kˣ := ⋯.unit
yu : Kˣ := ⋯.unit
hxmem : xu ∈ rootsOfUnity ⟨k, hkpos⟩ K
hymem : yu ∈ rootsOfUnity ⟨k, hkpos⟩ K
hxuord : orderOf ⟨xu, hxmem⟩ = p
hyuord : orderOf ⟨yu, hymem⟩ = q
g : ↥(rootsOfUnity ⟨k, hkpos⟩ K)
hg : ∀ (y : ↥(rootsOfUnity ⟨k, hkpos⟩ K)), y ∈ Submonoid.powers g
nx : ℕ
hnx : (fun x => g ^ x) nx = ⟨xu, hxmem⟩
ny : ℕ
hny : (fun x => g ^ x) ny = ⟨yu, hymem⟩
H : orderOf g = k
hroot : IsPrimitiveRoot ↑↑g ↑⟨k, hkpos⟩
this : IsCyclotomicExtension {⟨k, hkpos⟩} ℚ ↥(Algebra.adjoin ℚ {↑↑g})
⊢ (lcm p q).totient = FiniteDimensional.finrank ℚ ↥(Subalgebra.toSubmodule (Algebra.adjoin ℚ {↑↑g}))
Theorem: contains_two_primitive_roots
Proof state before:
case h.e'_3
p✝ : ℕ+
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p✝
inst✝¹ : NumberField K
p q : ℕ
x y : K
inst✝ : FiniteDimensional ℚ K
hx : IsPrimitiveRoot x p
hy : IsPrimitiveRoot y q
hppos : p > 0
hqpos : q > 0
k : ℕ := lcm p q
hkpos : 0 < k
xu : Kˣ := ⋯.unit
yu : Kˣ := ⋯.unit
hxmem : xu ∈ rootsOfUnity ⟨k, hkpos⟩ K
hymem : yu ∈ rootsOfUnity ⟨k, hkpos⟩ K
hxuord : orderOf ⟨xu, hxmem⟩ = p
hyuord : orderOf ⟨yu, hymem⟩ = q
g : ↥(rootsOfUnity ⟨k, hkpos⟩ K)
hg : ∀ (y : ↥(rootsOfUnity ⟨k, hkpos⟩ K)), y ∈ Submonoid.powers g
nx : ℕ
hnx : (fun x => g ^ x) nx = ⟨xu, hxmem⟩
ny : ℕ
hny : (fun x => g ^ x) ny = ⟨yu, hymem⟩
H : orderOf g = k
hroot : IsPrimitiveRoot ↑↑g ↑⟨k, hkpos⟩
this : IsCyclotomicExtension {⟨k, hkpos⟩} ℚ ↥(Algebra.adjoin ℚ {↑↑g})
⊢ (lcm p q).totient = FiniteDimensional.finrank ℚ ↥(Subalgebra.toSubmodule (Algebra.adjoin ℚ {↑↑g}))
Tactic:
simpa using
  (IsCyclotomicExtension.finrank (Algebra.adjoin ℚ ({g.1.1} : Set K))
      (cyclotomic.irreducible_rat (PNat.pos ⟨k, hkpos⟩))).symm
Proof state after:
no goals
Theorem: contains_two_primitive_roots
Proof state before:
case inl
p : ℕ+
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝¹ : NumberField K
q : ℕ
x y : K
inst✝ : FiniteDimensional ℚ K
hy : IsPrimitiveRoot y q
hx : IsPrimitiveRoot x 0
⊢ (lcm 0 q).totient ≤ FiniteDimensional.finrank ℚ K
Tactic:
simp
Proof state after:
no goals
Theorem: contains_two_primitive_roots
Proof state before:
case inr.inl
p✝ : ℕ+
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p✝
inst✝¹ : NumberField K
p : ℕ
x y : K
inst✝ : FiniteDimensional ℚ K
hx : IsPrimitiveRoot x p
hppos : p > 0
hy : IsPrimitiveRoot y 0
⊢ (lcm p 0).totient ≤ FiniteDimensional.finrank ℚ K
Tactic:
simp
Proof state after:
no goals
Theorem: contains_two_primitive_roots
Proof state before:
p✝ : ℕ+
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p✝
inst✝¹ : NumberField K
p q : ℕ
x y : K
inst✝ : FiniteDimensional ℚ K
hx : IsPrimitiveRoot x p
hy : IsPrimitiveRoot y q
hppos : p > 0
hqpos : q > 0
k : ℕ := lcm p q
hkpos : 0 < k
xu : Kˣ := ⋯.unit
yu : Kˣ := ⋯.unit
⊢ xu ∈ rootsOfUnity ⟨k, hkpos⟩ K
Tactic:
rw [mem_rootsOfUnity, PNat.mk_coe, ← Units.val_eq_one, Units.val_pow_eq_pow_val,
  IsUnit.unit_spec]
Proof state after:
p✝ : ℕ+
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p✝
inst✝¹ : NumberField K
p q : ℕ
x y : K
inst✝ : FiniteDimensional ℚ K
hx : IsPrimitiveRoot x p
hy : IsPrimitiveRoot y q
hppos : p > 0
hqpos : q > 0
k : ℕ := lcm p q
hkpos : 0 < k
xu : Kˣ := ⋯.unit
yu : Kˣ := ⋯.unit
⊢ x ^ k = 1
Theorem: contains_two_primitive_roots
Proof state before:
p✝ : ℕ+
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p✝
inst✝¹ : NumberField K
p q : ℕ
x y : K
inst✝ : FiniteDimensional ℚ K
hx : IsPrimitiveRoot x p
hy : IsPrimitiveRoot y q
hppos : p > 0
hqpos : q > 0
k : ℕ := lcm p q
hkpos : 0 < k
xu : Kˣ := ⋯.unit
yu : Kˣ := ⋯.unit
⊢ x ^ k = 1
Tactic:
exact (hx.pow_eq_one_iff_dvd _).2 (dvd_lcm_left _ _)
Proof state after:
no goals
Theorem: contains_two_primitive_roots
Proof state before:
p✝ : ℕ+
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p✝
inst✝¹ : NumberField K
p q : ℕ
x y : K
inst✝ : FiniteDimensional ℚ K
hx : IsPrimitiveRoot x p
hy : IsPrimitiveRoot y q
hppos : p > 0
hqpos : q > 0
k : ℕ := lcm p q
hkpos : 0 < k
xu : Kˣ := ⋯.unit
yu : Kˣ := ⋯.unit
hxmem : xu ∈ rootsOfUnity ⟨k, hkpos⟩ K
⊢ yu ∈ rootsOfUnity ⟨k, hkpos⟩ K
Tactic:
rw [mem_rootsOfUnity, PNat.mk_coe, ← Units.val_eq_one, Units.val_pow_eq_pow_val,
  IsUnit.unit_spec]
Proof state after:
p✝ : ℕ+
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p✝
inst✝¹ : NumberField K
p q : ℕ
x y : K
inst✝ : FiniteDimensional ℚ K
hx : IsPrimitiveRoot x p
hy : IsPrimitiveRoot y q
hppos : p > 0
hqpos : q > 0
k : ℕ := lcm p q
hkpos : 0 < k
xu : Kˣ := ⋯.unit
yu : Kˣ := ⋯.unit
hxmem : xu ∈ rootsOfUnity ⟨k, hkpos⟩ K
⊢ y ^ k = 1