internlm/Lean-Github huggingface dataset:
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
⊢ y ^ k = 1
Tactic:
exact (hy.pow_eq_one_iff_dvd _).2 (dvd_lcm_right _ _)
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
hymem : yu ∈ rootsOfUnity ⟨k, hkpos⟩ K
⊢ orderOf ⟨xu, hxmem⟩ = p
Tactic:
rw [← orderOf_injective (rootsOfUnity ⟨k, hkpos⟩ K).subtype Subtype.coe_injective,
  Subgroup.coeSubtype, Subgroup.coe_mk, ← orderOf_units, 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
hymem : yu ∈ rootsOfUnity ⟨k, hkpos⟩ K
⊢ orderOf x = p
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
hymem : yu ∈ rootsOfUnity ⟨k, hkpos⟩ K
⊢ orderOf x = p
Tactic:
exact hx.eq_orderOf.symm
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
hymem : yu ∈ rootsOfUnity ⟨k, hkpos⟩ K
hxuord : orderOf ⟨xu, hxmem⟩ = p
⊢ orderOf ⟨yu, hymem⟩ = q
Tactic:
rw [← orderOf_injective (rootsOfUnity ⟨k, hkpos⟩ K).subtype Subtype.coe_injective,
  Subgroup.coeSubtype, Subgroup.coe_mk, ← orderOf_units, 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
hymem : yu ∈ rootsOfUnity ⟨k, hkpos⟩ K
hxuord : orderOf ⟨xu, hxmem⟩ = p
⊢ orderOf y = q
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
hymem : yu ∈ rootsOfUnity ⟨k, hkpos⟩ K
hxuord : orderOf ⟨xu, hxmem⟩ = p
⊢ orderOf y = q
Tactic:
exact hy.eq_orderOf.symm
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
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⟩
⊢ orderOf g = k
Tactic:
refine' Nat.dvd_antisymm (orderOf_dvd_of_pow_eq_one _) (Nat.lcm_dvd _ _)
Proof state after:
case refine'_1
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⟩
⊢ g ^ k = 1

case refine'_2
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⟩
⊢ p ∣ orderOf g

case refine'_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⟩
⊢ q ∣ orderOf g
Theorem: contains_two_primitive_roots
Proof state before:
case refine'_1
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⟩
⊢ g ^ k = 1
Tactic:
have := (mem_rootsOfUnity _ _).1 g.2
Proof state after:
case refine'_1
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⟩
this : ↑g ^ ↑⟨k, hkpos⟩ = 1
⊢ g ^ k = 1
Theorem: contains_two_primitive_roots
Proof state before:
case refine'_1
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⟩
this : ↑g ^ ↑⟨k, hkpos⟩ = 1
⊢ g ^ k = 1
Tactic:
simp only [PNat.mk_coe] at this
Proof state after:
case refine'_1
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⟩
this : ↑g ^ k = 1
⊢ g ^ k = 1
Theorem: contains_two_primitive_roots
Proof state before:
case refine'_1
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⟩
this : ↑g ^ k = 1
⊢ g ^ k = 1
Tactic:
exact_mod_cast this
Proof state after:
no goals
Theorem: contains_two_primitive_roots
Proof state before:
case refine'_2
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⟩
⊢ p ∣ orderOf g
Tactic:
rw [← hxuord, ← hnx, orderOf_pow]
Proof state after:
case refine'_2
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⟩
⊢ orderOf g / (orderOf g).gcd nx ∣ orderOf g
Theorem: contains_two_primitive_roots
Proof state before:
case refine'_2
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⟩
⊢ orderOf g / (orderOf g).gcd nx ∣ orderOf g
Tactic:
exact Nat.div_dvd_of_dvd ((orderOf g).gcd_dvd_left nx)
Proof state after:
no goals
Theorem: contains_two_primitive_roots
Proof state before:
case refine'_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⟩
⊢ q ∣ orderOf g
Tactic:
rw [← hyuord, ← hny, orderOf_pow]
Proof state after:
case refine'_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⟩
⊢ orderOf g / (orderOf g).gcd ny ∣ orderOf g
Theorem: contains_two_primitive_roots
Proof state before:
case refine'_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⟩
⊢ orderOf g / (orderOf g).gcd ny ∣ orderOf g
Tactic:
exact Nat.div_dvd_of_dvd ((orderOf g).gcd_dvd_left ny)
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
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
⊢ k = ↑⟨k, hkpos⟩
Tactic:
simp
Proof state after:
no goals
Theorem: totient_le_one_dvd_two
Proof state before:
p : ℕ+
K : Type ?u.47922
inst✝¹ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝ : NumberField K
a : ℕ
han : 0 < a
ha : a.totient ≤ 1
⊢ a ∣ 2
Tactic:
cases' Nat.totient_eq_one_iff.1 (show a.totient = 1 by linarith [Nat.totient_pos.2 han]) with h
    h <;>
  simp [h]
Proof state after:
no goals
Theorem: totient_le_one_dvd_two
Proof state before:
p : ℕ+
K : Type ?u.47922
inst✝¹ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝ : NumberField K
a : ℕ
han : 0 < a
ha : a.totient ≤ 1
⊢ a.totient = 1
Tactic:
linarith [Nat.totient_pos.2 han]
Proof state after:
no goals
Theorem: eq_one_mod_one_sub
Proof state before:
p : ℕ+
K : Type ?u.53883
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝¹ : NumberField K
A : Type u_1
inst✝ : CommRing A
t : A
⊢ (algebraMap A (A ⧸ Ideal.span {t - 1})) t = 1
Tactic:
rw [← map_one <| algebraMap A <| A ⧸ Ideal.span ({t - 1} : Set A), ← sub_eq_zero, ← map_sub,
  Ideal.Quotient.algebraMap_eq, Ideal.Quotient.eq_zero_iff_mem]
Proof state after:
p : ℕ+
K : Type ?u.53883
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝¹ : NumberField K
A : Type u_1
inst✝ : CommRing A
t : A
⊢ t - 1 ∈ Ideal.span {t - 1}
Theorem: eq_one_mod_one_sub
Proof state before:
p : ℕ+
K : Type ?u.53883
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝¹ : NumberField K
A : Type u_1
inst✝ : CommRing A
t : A
⊢ t - 1 ∈ Ideal.span {t - 1}
Tactic:
apply Ideal.subset_span
Proof state after:
case a
p : ℕ+
K : Type ?u.53883
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝¹ : NumberField K
A : Type u_1
inst✝ : CommRing A
t : A
⊢ t - 1 ∈ {t - 1}
Theorem: eq_one_mod_one_sub
Proof state before:
case a
p : ℕ+
K : Type ?u.53883
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝¹ : NumberField K
A : Type u_1
inst✝ : CommRing A
t : A
⊢ t - 1 ∈ {t - 1}
Tactic:
exact Set.mem_singleton _
Proof state after:
no goals
Theorem: IsPrimitiveRoot.eq_one_mod_sub_of_pow
Proof state before:
p : ℕ+
K : Type ?u.65835
inst✝³ : Field K
ζ✝ : K
hζ✝ : IsPrimitiveRoot ζ✝ ↑p
inst✝² : NumberField K
A : Type u_1
inst✝¹ : CommRing A
inst✝ : IsDomain A
ζ : A
hζ : IsPrimitiveRoot ζ ↑p
μ : A
hμ : μ ^ ↑p = 1
⊢ (algebraMap A (A ⧸ Ideal.span {ζ - 1})) μ = 1
Tactic:
obtain ⟨k, -, rfl⟩ := hζ.eq_pow_of_pow_eq_one hμ p.pos
Proof state after:
case intro.intro
p : ℕ+
K : Type ?u.65835
inst✝³ : Field K
ζ✝ : K
hζ✝ : IsPrimitiveRoot ζ✝ ↑p
inst✝² : NumberField K
A : Type u_1
inst✝¹ : CommRing A
inst✝ : IsDomain A
ζ : A
hζ : IsPrimitiveRoot ζ ↑p
k : ℕ
hμ : (ζ ^ k) ^ ↑p = 1
⊢ (algebraMap A (A ⧸ Ideal.span {ζ - 1})) (ζ ^ k) = 1
Theorem: IsPrimitiveRoot.eq_one_mod_sub_of_pow
Proof state before:
case intro.intro
p : ℕ+
K : Type ?u.65835
inst✝³ : Field K
ζ✝ : K
hζ✝ : IsPrimitiveRoot ζ✝ ↑p
inst✝² : NumberField K
A : Type u_1
inst✝¹ : CommRing A
inst✝ : IsDomain A
ζ : A
hζ : IsPrimitiveRoot ζ ↑p
k : ℕ
hμ : (ζ ^ k) ^ ↑p = 1
⊢ (algebraMap A (A ⧸ Ideal.span {ζ - 1})) (ζ ^ k) = 1
Tactic:
rw [map_pow, eq_one_mod_one_sub, one_pow]
Proof state after:
no goals
Theorem: aux
Proof state before:
p : ℕ+
K : Type u_1
inst✝¹ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝ : NumberField K
t : ℕ
l : 𝓞 K
f : Fin t → ℤ
μ : K
hμ : IsPrimitiveRoot μ ↑p
h : ∑ x : Fin t, f x • ⟨μ, ⋯⟩ ^ ↑x = l
⊢ (algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1})) l = ∑ x : Fin t, ↑(f x)
Tactic:
apply_fun algebraMap (𝓞 K) (𝓞 K ⧸ I) at h
Proof state after:
p : ℕ+
K : Type u_1
inst✝¹ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝ : NumberField K
t : ℕ
l : 𝓞 K
f : Fin t → ℤ
μ : K
hμ : IsPrimitiveRoot μ ↑p
h :
  (algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1})) (∑ x : Fin t, f x • ⟨μ, ⋯⟩ ^ ↑x) =
    (algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1})) l
⊢ (algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1})) l = ∑ x : Fin t, ↑(f x)
Theorem: aux
Proof state before:
p : ℕ+
K : Type u_1
inst✝¹ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝ : NumberField K
t : ℕ
l : 𝓞 K
f : Fin t → ℤ
μ : K
hμ : IsPrimitiveRoot μ ↑p
h :
  (algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1})) (∑ x : Fin t, f x • ⟨μ, ⋯⟩ ^ ↑x) =
    (algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1})) l
⊢ (algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1})) l = ∑ x : Fin t, ↑(f x)
Tactic:
simp only [map_sum, map_zsmul] at h
Proof state after:
p : ℕ+
K : Type u_1
inst✝¹ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝ : NumberField K
t : ℕ
l : 𝓞 K
f : Fin t → ℤ
μ : K
hμ : IsPrimitiveRoot μ ↑p
h :
  ∑ x : Fin t, f x • (algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1})) (⟨μ, ⋯⟩ ^ ↑x) =
    (algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1})) l
⊢ (algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1})) l = ∑ x : Fin t, ↑(f x)
Theorem: aux
Proof state before:
p : ℕ+
K : Type u_1
inst✝¹ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝ : NumberField K
t : ℕ
l : 𝓞 K
f : Fin t → ℤ
μ : K
hμ : IsPrimitiveRoot μ ↑p
h :
  ∑ x : Fin t, f x • (algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1})) (⟨μ, ⋯⟩ ^ ↑x) =
    (algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1})) l
⊢ (algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1})) l = ∑ x : Fin t, ↑(f x)
Tactic:
convert h.symm using 1
Proof state after:
case h.e'_3
p : ℕ+
K : Type u_1
inst✝¹ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝ : NumberField K
t : ℕ
l : 𝓞 K
f : Fin t → ℤ
μ : K
hμ : IsPrimitiveRoot μ ↑p
h :
  ∑ x : Fin t, f x • (algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1})) (⟨μ, ⋯⟩ ^ ↑x) =
    (algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1})) l
⊢ ∑ x : Fin t, ↑(f x) = ∑ x : Fin t, f x • (algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1})) (⟨μ, ⋯⟩ ^ ↑x)
Theorem: aux
Proof state before:
case h.e'_3
p : ℕ+
K : Type u_1
inst✝¹ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝ : NumberField K
t : ℕ
l : 𝓞 K
f : Fin t → ℤ
μ : K
hμ : IsPrimitiveRoot μ ↑p
h :
  ∑ x : Fin t, f x • (algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1})) (⟨μ, ⋯⟩ ^ ↑x) =
    (algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1})) l
⊢ ∑ x : Fin t, ↑(f x) = ∑ x : Fin t, f x • (algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1})) (⟨μ, ⋯⟩ ^ ↑x)
Tactic:
congr
Proof state after:
case h.e'_3.e_f
p : ℕ+
K : Type u_1
inst✝¹ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝ : NumberField K
t : ℕ
l : 𝓞 K
f : Fin t → ℤ
μ : K
hμ : IsPrimitiveRoot μ ↑p
h :
  ∑ x : Fin t, f x • (algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1})) (⟨μ, ⋯⟩ ^ ↑x) =
    (algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1})) l
⊢ (fun x => ↑(f x)) = fun x => f x • (algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1})) (⟨μ, ⋯⟩ ^ ↑x)
Theorem: aux
Proof state before:
case h.e'_3.e_f
p : ℕ+
K : Type u_1
inst✝¹ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝ : NumberField K
t : ℕ
l : 𝓞 K
f : Fin t → ℤ
μ : K
hμ : IsPrimitiveRoot μ ↑p
h :
  ∑ x : Fin t, f x • (algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1})) (⟨μ, ⋯⟩ ^ ↑x) =
    (algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1})) l
⊢ (fun x => ↑(f x)) = fun x => f x • (algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1})) (⟨μ, ⋯⟩ ^ ↑x)
Tactic:
funext x
Proof state after:
case h.e'_3.e_f.h
p : ℕ+
K : Type u_1
inst✝¹ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝ : NumberField K
t : ℕ
l : 𝓞 K
f : Fin t → ℤ
μ : K
hμ : IsPrimitiveRoot μ ↑p
h :
  ∑ x : Fin t, f x • (algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1})) (⟨μ, ⋯⟩ ^ ↑x) =
    (algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1})) l
x : Fin t
⊢ ↑(f x) = f x • (algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1})) (⟨μ, ⋯⟩ ^ ↑x)
Theorem: aux
Proof state before:
case h.e'_3.e_f.h
p : ℕ+
K : Type u_1
inst✝¹ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝ : NumberField K
t : ℕ
l : 𝓞 K
f : Fin t → ℤ
μ : K
hμ : IsPrimitiveRoot μ ↑p
h :
  ∑ x : Fin t, f x • (algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1})) (⟨μ, ⋯⟩ ^ ↑x) =
    (algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1})) l
x : Fin t
⊢ ↑(f x) = f x • (algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1})) (⟨μ, ⋯⟩ ^ ↑x)
Tactic:
have : (⟨μ, hμ.isIntegral p.pos⟩ : 𝓞 K) ^ (p : ℕ) = 1 := by
  ext
  push_cast
  exact hμ.pow_eq_one
Proof state after:
case h.e'_3.e_f.h
p : ℕ+
K : Type u_1
inst✝¹ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝ : NumberField K
t : ℕ
l : 𝓞 K
f : Fin t → ℤ
μ : K
hμ : IsPrimitiveRoot μ ↑p
h :
  ∑ x : Fin t, f x • (algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1})) (⟨μ, ⋯⟩ ^ ↑x) =
    (algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1})) l
x : Fin t
this : ⟨μ, ⋯⟩ ^ ↑p = 1
⊢ ↑(f x) = f x • (algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1})) (⟨μ, ⋯⟩ ^ ↑x)