awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.RootsOfUnity.Minpoly
Goal:
K : Type u_1
inst : CommRing K
μ : K
inst_1 : IsDomain K
inst_2 : CharZero K
m n a p : ℕ
h_1 : a ≠ 0
h : IsPrimitiveRoot μ n
hcop : (p * a).Coprime n
hprime : Nat.Prime p
⊢ ¬p ∣ n

Tactic:
have hdiv := (Nat.Prime.coprime_iff_not_dvd hprime).1 (Nat.Coprime.coprime_mul_right hcop)
-- Module: Mathlib.RingTheory.RootsOfUnity.Minpoly
Goal:
K : Type u_1
inst : CommRing K
μ : K
inst_1 : IsDomain K
inst_2 : CharZero K
m n a p : ℕ
h_1 : a ≠ 0
h : IsPrimitiveRoot μ n
hcop : (p * a).Coprime n
hprime : Nat.Prime p
hdiv : ¬p ∣ n
⊢ Fact (Nat.Prime p)

Tactic:
haveI := Fact.mk hprime
-- Module: Mathlib.RingTheory.RootsOfUnity.Minpoly
Goal:
K : Type u_1
inst : CommRing K
μ : K
inst_1 : IsDomain K
inst_2 : CharZero K
m n a p : ℕ
h_1 : a ≠ 0
h : IsPrimitiveRoot μ n
hcop : (p * a).Coprime n
hprime : Nat.Prime p
hdiv : ¬p ∣ n
this : Fact (Nat.Prime p)
refine_3 : Eq (α := ℤ[X]) (minpoly ℤ ((μ ^ a) ^ p)) (minpoly ℤ (μ ^ (p * a)))
⊢ Eq (α := ℤ[X]) (minpoly ℤ (μ ^ a)) (minpoly ℤ (μ ^ (p * a)))

Tactic:
rw [minpoly_eq_pow (h.pow_of_coprime a (Nat.Coprime.coprime_mul_left hcop)) hdiv]

Premises used: IsPrimitiveRoot.pow_of_coprime, Nat.Coprime.coprime_mul_left, IsPrimitiveRoot.minpoly_eq_pow
-- Module: Mathlib.RingTheory.RootsOfUnity.Minpoly
Goal:
K : Type u_1
inst : CommRing K
μ : K
inst_1 : IsDomain K
inst_2 : CharZero K
m n a p : ℕ
h_1 : a ≠ 0
h : IsPrimitiveRoot μ n
hcop : (p * a).Coprime n
hprime : Nat.Prime p
hdiv : ¬p ∣ n
this : Fact (Nat.Prime p)
refine_3 : (μ ^ a) ^ p = μ ^ (p * a)
⊢ Eq (α := ℤ[X]) (minpoly ℤ ((μ ^ a) ^ p)) (minpoly ℤ (μ ^ (p * a)))

Tactic:
congr 1
-- Module: Mathlib.RingTheory.RootsOfUnity.Minpoly
Goal:
K : Type u_1
inst : CommRing K
μ : K
inst_1 : IsDomain K
inst_2 : CharZero K
m n a p : ℕ
h_1 : a ≠ 0
h : IsPrimitiveRoot μ n
hcop : (p * a).Coprime n
hprime : Nat.Prime p
hdiv : ¬p ∣ n
this : Fact (Nat.Prime p)
⊢ (μ ^ a) ^ p = μ ^ (p * a)

Tactic:
ring
-- Module: Mathlib.RingTheory.RootsOfUnity.Minpoly
Goal:
n : ℕ
K : Type u_1
inst : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst_1 : IsDomain K
inst_2 : CharZero K
m : ℕ
hcop : m.Coprime n
simp : eval₂ (Int.castRingHom K) (μ ^ m) (minpoly ℤ (μ ^ m)) = 0
⊢ IsRoot (map (Int.castRingHom K) (minpoly ℤ μ)) (μ ^ m)

Tactic:
simp only [minpoly_eq_pow_coprime h hcop, IsRoot.def, eval_map]

Premises used: Polynomial.eval_map, IsPrimitiveRoot.minpoly_eq_pow_coprime, Polynomial.IsRoot.def
-- Module: Mathlib.RingTheory.RootsOfUnity.Minpoly
Goal:
n : ℕ
K : Type u_1
inst : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst_1 : IsDomain K
inst_2 : CharZero K
m : ℕ
hcop : m.Coprime n
⊢ eval₂ (Int.castRingHom K) (μ ^ m) (minpoly ℤ (μ ^ m)) = 0

Tactic:
minpoly.aeval ℤ (μ ^ m)

Premises used: MonoidHomClass.toMonoidHom, Int, minpoly.aeval, HPow.hPow, RingHomClass.toRingHom
-- Module: Mathlib.RingTheory.RootsOfUnity.Minpoly
Goal:
n : ℕ
K : Type u_1
inst : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst_1 : IsDomain K
inst_2 : CharZero K
m : ℕ
hcop : m.Coprime n
⊢ eval₂ (Int.castRingHom K) (μ ^ m) (minpoly ℤ (μ ^ m)) = 0

Tactic:
exact minpoly.aeval ℤ (μ ^ m)

Premises used: Int, minpoly.aeval, HPow.hPow
-- Module: Mathlib.RingTheory.RootsOfUnity.Minpoly
Goal:
n : ℕ
K : Type u_1
inst : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst_1 : IsDomain K
inst_2 : CharZero K
inst_3 : DecidableEq K
pos : ∀ (hn : n = 0), primitiveRoots n K ⊆ Multiset.toFinset (roots (map (Int.castRingHom K) (minpoly ℤ μ)))
neg : ∀ (hn : ¬n = 0), primitiveRoots n K ⊆ Multiset.toFinset (roots (map (Int.castRingHom K) (minpoly ℤ μ)))
⊢ primitiveRoots n K ⊆ Multiset.toFinset (roots (map (Int.castRingHom K) (minpoly ℤ μ)))

Tactic:
by_cases hn : n = 0
-- Module: Mathlib.RingTheory.RootsOfUnity.Minpoly
Goal:
n : ℕ
K : Type u_1
inst : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst_1 : IsDomain K
inst_2 : CharZero K
inst_3 : DecidableEq K
hn : n = 0
⊢ primitiveRoots n K ⊆ Multiset.toFinset (roots (map (Int.castRingHom K) (minpoly ℤ μ)))

Tactic:
simp_all
-- Module: Mathlib.RingTheory.RootsOfUnity.Minpoly
Goal:
n : ℕ
K : Type u_1
inst : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst_1 : IsDomain K
inst_2 : CharZero K
inst_3 : DecidableEq K
hn : ¬n = 0
⊢ NeZero n

Tactic:
have : NeZero n := ⟨hn⟩
-- Module: Mathlib.RingTheory.RootsOfUnity.Minpoly
Goal:
n : ℕ
K : Type u_1
inst : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst_1 : IsDomain K
inst_2 : CharZero K
inst_3 : DecidableEq K
hn : ¬n = 0
this : NeZero n
⊢ 0 < n

Tactic:
have hpos := Nat.pos_of_ne_zero hn
-- Module: Mathlib.RingTheory.RootsOfUnity.Minpoly
Goal:
n : ℕ
K : Type u_1
inst : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst_1 : IsDomain K
inst_2 : CharZero K
inst_3 : DecidableEq K
hn : ¬n = 0
this : NeZero n
hpos : 0 < n
x : K
hx : x ∈ primitiveRoots n K
neg :
  ∀ m < n,
    ∀ (hcop : m.Coprime n) (hx : μ ^ m ∈ primitiveRoots n K),
      Membership.mem (γ := Finset K) (Multiset.toFinset (roots (map (Int.castRingHom K) (minpoly ℤ μ)))) (μ ^ m)
⊢ Membership.mem (γ := Finset K) (Multiset.toFinset (roots (map (Int.castRingHom K) (minpoly ℤ μ)))) x

Tactic:
obtain ⟨m, _, hcop, rfl⟩ := (isPrimitiveRoot_iff h).1 ((mem_primitiveRoots hpos).1 hx)

Premises used: IsPrimitiveRoot.isPrimitiveRoot_iff, mem_primitiveRoots, Iff.mp, rfl
-- Module: Mathlib.RingTheory.RootsOfUnity.Minpoly
Goal:
n : ℕ
K : Type u_1
inst : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst_1 : IsDomain K
inst_2 : CharZero K
inst_3 : DecidableEq K
hn : ¬n = 0
this : NeZero n
hpos : 0 < n
m : ℕ
left : m < n
hcop : m.Coprime n
hx : μ ^ m ∈ primitiveRoots n K
neg : Membership.mem (γ := Multiset K) (roots (map (Int.castRingHom K) (minpoly ℤ μ))) (μ ^ m)
⊢ Membership.mem (γ := Finset K) (Multiset.toFinset (roots (map (Int.castRingHom K) (minpoly ℤ μ)))) (μ ^ m)

Tactic:
simp only [Multiset.mem_toFinset]

Premises used: Multiset.mem_toFinset
-- Module: Mathlib.RingTheory.RootsOfUnity.Minpoly
Goal:
n : ℕ
K : Type u_1
inst : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst_1 : IsDomain K
inst_2 : CharZero K
inst_3 : DecidableEq K
hn : ¬n = 0
this : NeZero n
hpos : 0 < n
m : ℕ
left : m < n
hcop : m.Coprime n
hx : μ ^ m ∈ primitiveRoots n K
⊢ IsRoot (map (Int.castRingHom K) (minpoly ℤ μ)) (μ ^ m)

Tactic:
pow_isRoot_minpoly h hcop

Premises used: IsPrimitiveRoot.pow_isRoot_minpoly
-- Module: Mathlib.RingTheory.RootsOfUnity.Minpoly
Goal:
n : ℕ
K : Type u_1
inst : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst_1 : IsDomain K
inst_2 : CharZero K
inst_3 : DecidableEq K
hn : ¬n = 0
this : NeZero n
hpos : 0 < n
m : ℕ
left : m < n
hcop : m.Coprime n
hx : μ ^ m ∈ primitiveRoots n K
a :
  Membership.mem (γ := Multiset K) (roots (map (Int.castRingHom K) (minpoly ℤ μ))) (μ ^ m) ↔
    IsRoot (map (Int.castRingHom K) (minpoly ℤ μ)) (μ ^ m)
⊢ Membership.mem (γ := Multiset K) (roots (map (Int.castRingHom K) (minpoly ℤ μ))) (μ ^ m)

Tactic:
convert! pow_isRoot_minpoly h hcop using 0

Premises used: IsPrimitiveRoot.pow_isRoot_minpoly
-- Module: Mathlib.RingTheory.RootsOfUnity.Minpoly
Goal:
n : ℕ
K : Type u_1
inst : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst_1 : IsDomain K
inst_2 : CharZero K
inst_3 : DecidableEq K
hn : ¬n = 0
this : NeZero n
hpos : 0 < n
m : ℕ
left : m < n
hcop : m.Coprime n
hx : μ ^ m ∈ primitiveRoots n K
a : Ne.{u_1 + 1} (α := K[X]) (map (Int.castRingHom K) (minpoly ℤ μ)) 0
⊢ Membership.mem (γ := Multiset K) (roots (map (Int.castRingHom K) (minpoly ℤ μ))) (μ ^ m) ↔
    IsRoot (map (Int.castRingHom K) (minpoly ℤ μ)) (μ ^ m)

Tactic:
rw [← mem_roots]

Premises used: Polynomial.mem_roots
-- Module: Mathlib.RingTheory.RootsOfUnity.Minpoly
Goal:
n : ℕ
K : Type u_1
inst : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst_1 : IsDomain K
inst_2 : CharZero K
inst_3 : DecidableEq K
hn : ¬n = 0
this : NeZero n
hpos : 0 < n
m : ℕ
left : m < n
hcop : m.Coprime n
hx : μ ^ m ∈ primitiveRoots n K
⊢ Ne.{u_1 + 1} (α := K[X]) (map (Int.castRingHom K) (minpoly ℤ μ)) 0

Tactic:
map_monic_ne_zero <| minpoly.monic <| isIntegral h hpos

Premises used: minpoly.monic, IsPrimitiveRoot.isIntegral, Polynomial.map_monic_ne_zero
-- Module: Mathlib.RingTheory.RootsOfUnity.Minpoly
Goal:
n : ℕ
K : Type u_1
inst : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst_1 : IsDomain K
inst_2 : CharZero K
inst_3 : DecidableEq K
hn : ¬n = 0
this : NeZero n
hpos : 0 < n
m : ℕ
left : m < n
hcop : m.Coprime n
hx : μ ^ m ∈ primitiveRoots n K
⊢ Ne.{u_1 + 1} (α := K[X]) (map (Int.castRingHom K) (minpoly ℤ μ)) 0

Tactic:
exact map_monic_ne_zero <| minpoly.monic <| isIntegral h hpos

Premises used: minpoly.monic, IsPrimitiveRoot.isIntegral, Polynomial.map_monic_ne_zero
-- Module: Mathlib.RingTheory.RootsOfUnity.Minpoly
Goal:
n : ℕ
K : Type u_1
inst : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst_1 : IsDomain K
inst_2 : CharZero K
P : ℤ[X] := minpoly ℤ μ
P_K : K[X] := map (Int.castRingHom K) P
⊢ n.totient = (primitiveRoots n K).card

Tactic:
h.card_primitiveRoots.symm

Premises used: IsPrimitiveRoot.card_primitiveRoots, Eq.symm
-- Module: Mathlib.RingTheory.RootsOfUnity.Minpoly
Goal:
n : ℕ
K : Type u_1
inst : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst_1 : IsDomain K
inst_2 : CharZero K
P : ℤ[X] := minpoly ℤ μ
P_K : K[X] := map (Int.castRingHom K) P
⊢ (primitiveRoots n K).card ≤ P_K.roots.toFinset.card

Tactic:
Finset.card_le_card (is_roots_of_minpoly h)

Premises used: IsPrimitiveRoot.is_roots_of_minpoly, Finset.card_le_card
-- Module: Mathlib.RingTheory.RootsOfUnity.Minpoly
Goal:
n : ℕ
K : Type u_1
inst : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst_1 : IsDomain K
inst_2 : CharZero K
P : ℤ[X] := minpoly ℤ μ
P_K : K[X] := map (Int.castRingHom K) P
⊢ P_K.roots.toFinset.card ≤ P_K.roots.card

Tactic:
Multiset.toFinset_card_le _

Premises used: Multiset.toFinset_card_le
-- Module: Mathlib.RingTheory.RootsOfUnity.Minpoly
Goal:
n : ℕ
K : Type u_1
inst : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst_1 : IsDomain K
inst_2 : CharZero K
P : ℤ[X] := minpoly ℤ μ
P_K : K[X] := map (Int.castRingHom K) P
⊢ P_K.roots.card ≤ P_K.natDegree

Tactic:
card_roots' _

Premises used: Polynomial.card_roots'
-- Module: Mathlib.RingTheory.RootsOfUnity.Minpoly
Goal:
n : ℕ
K : Type u_1
inst : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst_1 : IsDomain K
inst_2 : CharZero K
P : ℤ[X] := minpoly ℤ μ
P_K : K[X] := map (Int.castRingHom K) P
⊢ P_K.natDegree ≤ P.natDegree

Tactic:
natDegree_map_le

Premises used: Polynomial.natDegree_map_le
-- Module: Mathlib.RingTheory.RootsOfUnity.Minpoly
Goal:
n : ℕ
K : Type u_1
inst : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst_1 : IsDomain K
inst_2 : CharZero K
P : ℤ[X] := minpoly ℤ μ
P_K : K[X] := map (Int.castRingHom K) P
⊢ n.totient ≤ natDegree (minpoly ℤ μ)

Tactic:
calc
    n.totient = (primitiveRoots n K).card := h.card_primitiveRoots.symm
    _ ≤ P_K.roots.toFinset.card := Finset.card_le_card (is_roots_of_minpoly h)
    _ ≤ Multiset.card P_K.roots := Multiset.toFinset_card_le _
    _ ≤ P_K.natDegree := card_roots' _
    _ ≤ P.natDegree := natDegree_map_le

Premises used: Multiset.toFinset, Polynomial.roots, IsPrimitiveRoot.is_roots_of_minpoly, Multiset.toFinset_card_le, Finset.card_le_card, Nat.totient, IsPrimitiveRoot.card_primitiveRoots, Polynomial.card_roots', Polynomial.natDegree_map_le, Finset.card, Multiset.card, primitiveRoots, Polynomial.natDegree, Eq.symm
-- Module: Mathlib.RingTheory.RootsOfUnity.Minpoly
Goal:
n : ℕ
K : Type u_1
inst : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst_1 : IsDomain K
inst_2 : CharZero K
let let₁ let₂ let₃ : n.totient ≤ natDegree (minpoly ℤ μ)
⊢ n.totient ≤ natDegree (minpoly ℤ μ)

Tactic:
classical
  let P : ℤ[X] := minpoly ℤ μ
  -- minimal polynomial of `μ`
  let P_K : K[X] := map (Int.castRingHom K) P
  -- minimal polynomial of `μ` sent to `K[X]`
  calc
    n.totient = (primitiveRoots n K).card := h.card_primitiveRoots.symm
    _ ≤ P_K.roots.toFinset.card := Finset.card_le_card (is_roots_of_minpoly h)
    _ ≤ Multiset.card P_K.roots := Multiset.toFinset_card_le _
    _ ≤ P_K.natDegree := card_roots' _
    _ ≤ P.natDegree := natDegree_map_le

Premises used: Multiset.toFinset_card_le, Nat.totient, IsPrimitiveRoot.card_primitiveRoots, Polynomial.card_roots', Polynomial.natDegree_map_le, Finset.card, primitiveRoots, Eq.symm
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
R : Type u_4
k : ℕ
inst : CommRing R
inst_1 : IsDomain R
ζ : R
h0 : 0 < k
rw : IsPrimitiveRoot ζ k → ζ ^ k = 1
⊢ ζ ∈ primitiveRoots k R ↔ IsPrimitiveRoot ζ k

Tactic:
rw [primitiveRoots, mem_filter, Multiset.mem_toFinset, mem_nthRoots h0, and_iff_right_iff_imp]

Premises used: and_iff_right_iff_imp, Finset.mem_filter, primitiveRoots, Polynomial.mem_nthRoots, Multiset.mem_toFinset
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
R : Type u_4
k : ℕ
inst : CommRing R
inst_1 : IsDomain R
ζ : R
h0 : 0 < k
⊢ IsPrimitiveRoot ζ k → ζ ^ k = 1

Tactic:
IsPrimitiveRoot.pow_eq_one

Premises used: IsPrimitiveRoot.pow_eq_one
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
R : Type u_4
k : ℕ
inst : CommRing R
inst_1 : IsDomain R
ζ : R
h0 : 0 < k
⊢ IsPrimitiveRoot ζ k → ζ ^ k = 1

Tactic:
exact IsPrimitiveRoot.pow_eq_one

Premises used: IsPrimitiveRoot.pow_eq_one
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
R : Type u_4
k : ℕ
inst : CommRing R
inst_1 : IsDomain R
ζ : R
h0 : 0 < k
rw :
  Membership.mem (γ := Finset R) ({ζ ∈ Multiset.toFinset (nthRoots k 1) | IsPrimitiveRoot ζ k}) ζ ↔ IsPrimitiveRoot ζ k
rw₁ : Membership.mem (γ := Finset R) (Multiset.toFinset (nthRoots k 1)) ζ ∧ IsPrimitiveRoot ζ k ↔ IsPrimitiveRoot ζ k
rw₂ : Membership.mem (γ := Multiset R) (nthRoots k 1) ζ ∧ IsPrimitiveRoot ζ k ↔ IsPrimitiveRoot ζ k
rw₃ : ζ ^ k = 1 ∧ IsPrimitiveRoot ζ k ↔ IsPrimitiveRoot ζ k
rw₄ rw₅ rw₆ : IsPrimitiveRoot ζ k → ζ ^ k = 1
⊢ ζ ∈ primitiveRoots k R ↔ IsPrimitiveRoot ζ k

Tactic:
classical
  rw [primitiveRoots, mem_filter, Multiset.mem_toFinset, mem_nthRoots h0, and_iff_right_iff_imp]
  exact IsPrimitiveRoot.pow_eq_one

Premises used: and_iff_right_iff_imp, Finset.mem_filter, primitiveRoots, Polynomial.mem_nthRoots, IsPrimitiveRoot.pow_eq_one, Multiset.mem_toFinset
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
R : Type u_4
inst : CommRing R
inst_1 : IsDomain R
rw : Eq.{u_4 + 1} (α := Finset R) ({ζ ∈ Multiset.toFinset (nthRoots 0 1) | IsPrimitiveRoot ζ 0}) ∅
rw₁ : Eq.{u_4 + 1} (α := Finset R) ({ζ ∈ Multiset.toFinset 0 | IsPrimitiveRoot ζ 0}) ∅
rw₂ : Eq.{u_4 + 1} (α := Finset R) ({ζ ∈ ∅ | IsPrimitiveRoot ζ 0}) ∅
rw₃ rw₄ : Eq.{u_4 + 1} (α := Finset R) ∅ ∅
⊢ primitiveRoots 0 R = ∅

Tactic:
rw [primitiveRoots, nthRoots_zero, Multiset.toFinset_zero, Finset.filter_empty]

Premises used: Finset.filter_empty, Polynomial.nthRoots_zero, Multiset.toFinset_zero, primitiveRoots
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
R : Type u_4
inst : CommRing R
inst_1 : IsDomain R
rw : Eq.{u_4 + 1} (α := Finset R) ({ζ ∈ Multiset.toFinset (nthRoots 0 1) | IsPrimitiveRoot ζ 0}) ∅
rw₁ : Eq.{u_4 + 1} (α := Finset R) ({ζ ∈ Multiset.toFinset 0 | IsPrimitiveRoot ζ 0}) ∅
rw₂ : Eq.{u_4 + 1} (α := Finset R) ({ζ ∈ ∅ | IsPrimitiveRoot ζ 0}) ∅
rw₃ rw₄ : Eq.{u_4 + 1} (α := Finset R) ∅ ∅
⊢ primitiveRoots 0 R = ∅

Tactic:
classical
  rw [primitiveRoots, nthRoots_zero, Multiset.toFinset_zero, Finset.filter_empty]

Premises used: Finset.filter_empty, Polynomial.nthRoots_zero, Multiset.toFinset_zero, primitiveRoots
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
R : Type u_4
k : ℕ
inst : CommRing R
inst_1 : IsDomain R
ζ : R
h : ζ ∈ primitiveRoots k R
hk : k = 0
⊢ IsPrimitiveRoot ζ k

Tactic:
simp [hk] at h
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
M : Type u_1
inst : CommMonoid M
k : ℕ
ζ : M
hk : 0 < k
h1 : ζ ^ k = 1
h : ∀ (l : ℕ), 0 < l → l < k → ζ ^ l ≠ 1
⊢ IsPrimitiveRoot ζ k

Tactic:
⟨h1, fun l hl ↦ ?_⟩

Premises used: IsPrimitiveRoot.mk
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
M : Type u_1
inst : CommMonoid M
k : ℕ
ζ : M
hk : 0 < k
h1 : ζ ^ k = 1
h : ∀ (l : ℕ), 0 < l → l < k → ζ ^ l ≠ 1
refine : ∀ (l : ℕ) (hl : ζ ^ l = 1), k ∣ l
⊢ IsPrimitiveRoot ζ k

Tactic:
refine ⟨h1, fun l hl ↦ ?_⟩
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
M : Type u_1
inst : CommMonoid M
k : ℕ
ζ : M
hk : 0 < k
h1 : ζ ^ k = 1
h : ∀ (l : ℕ), 0 < l → l < k → ζ ^ l ≠ 1
l : ℕ
hl : ζ ^ l = 1
suffices : k.gcd l = k
⊢ k ∣ l

Tactic:
suffices k.gcd l = k from this ▸ k.gcd_dvd_right l
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
M : Type u_1
inst : CommMonoid M
k : ℕ
ζ : M
hk : 0 < k
h1 : ζ ^ k = 1
h : ∀ (l : ℕ), 0 < l → l < k → ζ ^ l ≠ 1
l : ℕ
hl : ζ ^ l = 1
⊢ k.gcd l = k

Tactic:
(Nat.le_of_dvd hk (k.gcd_dvd_left l)).eq_of_not_lt fun h' ↦ ?_

Premises used: Nat.gcd_dvd_left, LE.le.eq_of_not_lt, Nat.le_of_dvd
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
M : Type u_1
inst : CommMonoid M
k : ℕ
ζ : M
hk : 0 < k
h1 : ζ ^ k = 1
h : ∀ (l : ℕ), 0 < l → l < k → ζ ^ l ≠ 1
l : ℕ
hl : ζ ^ l = 1
refine : ∀ (h' : k.gcd l < k), False
⊢ k.gcd l = k

Tactic:
refine (Nat.le_of_dvd hk (k.gcd_dvd_left l)).eq_of_not_lt fun h' ↦ ?_

Premises used: Nat.gcd_dvd_left, LE.le.eq_of_not_lt, Nat.le_of_dvd
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
M : Type u_1
inst : CommMonoid M
k : ℕ
ζ : M
hk : 0 < k
h1 : ζ ^ k = 1
h : ∀ (l : ℕ), 0 < l → l < k → ζ ^ l ≠ 1
l : ℕ
hl : ζ ^ l = 1
h' : k.gcd l < k
⊢ ζ ^ k.gcd l = 1

Tactic:
simp [h1, hl]
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
M : Type u_1
inst : CommMonoid M
k : ℕ
ζ : M
hk : 0 < k
h1 : ζ ^ k = 1
h : ∀ (l : ℕ), 0 < l → l < k → ζ ^ l ≠ 1
l : ℕ
hl : ζ ^ l = 1
h' : k.gcd l < k
⊢ False

Tactic:
exact h _ (Nat.gcd_pos_of_pos_left _ hk) h' (by simp [h1, hl])

Premises used: Nat.gcd_pos_of_pos_left
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
M : Type u_1
inst : CommMonoid M
inst_1 : Subsingleton M
x : M
⊢ IsPrimitiveRoot x 1

Tactic:
⟨Subsingleton.elim _ _, fun _ _ ↦ one_dvd _⟩

Premises used: IsPrimitiveRoot.mk, one_dvd, Subsingleton.elim
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
M : Type u_1
inst : CommMonoid M
k : ℕ
ζ : M
h : IsPrimitiveRoot ζ k
i : ℕ
⊢ ζ ^ (k * i) = 1

Tactic:
simp only [pow_mul, h.pow_eq_one, one_pow]

Premises used: one_pow, pow_mul, IsPrimitiveRoot.pow_eq_one
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
M : Type u_1
inst : CommMonoid M
k : ℕ
ζ : M
h : IsPrimitiveRoot ζ k
h0 : k ≠ 0
rw : ζ ^ (k - 1 + 1) = 1
rw₁ : ζ ^ k = 1
rw₂ rw₃ : Eq.{u_1 + 1} (α := M) 1 1
⊢ ζ * ζ ^ (k - 1) = 1

Tactic:
rw [← pow_succ', Nat.sub_one_add_one h0, h.pow_eq_one]

Premises used: Nat.sub_one_add_one, IsPrimitiveRoot.pow_eq_one, pow_succ'
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
M : Type u_1
inst : CommMonoid M
k : ℕ
ζ : M
h : IsPrimitiveRoot ζ k
h0 : k ≠ 0
⊢ IsOfFinOrder ζ

Tactic:
⟨k, Nat.ne_zero_iff_zero_lt.mp h0, (isPeriodicPt_mul_iff_pow_eq_one _).mpr h.pow_eq_one⟩

Premises used: Iff.mpr, Set.Mem, Nat.ne_zero_iff_zero_lt, setOf, isPeriodicPt_mul_iff_pow_eq_one, And.intro, Function.periodicPts, Exists.intro, Iff.mp, IsPrimitiveRoot.pow_eq_one, IsOfFinOrder
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
M : Type u_1
inst : CommMonoid M
k l : ℕ
ζ : M
h : IsPrimitiveRoot ζ k
h0 : l ≠ 0
hl : l < k
⊢ ζ ^ l ≠ 1

Tactic:
mt (Nat.le_of_dvd (Nat.pos_iff_ne_zero.mpr h0) ∘ h.dvd_of_pow_eq_one _) <| not_le_of_gt hl

Premises used: Iff.mpr, Nat.pos_iff_ne_zero, Function.comp, mt, IsPrimitiveRoot.dvd_of_pow_eq_one, not_le_of_gt, Nat.le_of_dvd
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
M : Type u_1
inst : CommMonoid M
k : ℕ
ζ : M
h : IsPrimitiveRoot ζ k
hk : 1 < k
⊢ ζ ≠ 1

Tactic:
h.pow_ne_one_of_pos_of_lt one_ne_zero hk ∘ (pow_one ζ).trans

Premises used: IsPrimitiveRoot.pow_ne_one_of_pos_of_lt, Function.comp, pow_one, one_ne_zero, Not, Eq.trans
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
M : Type u_1
inst : CommMonoid M
k : ℕ
ζ : M
h : IsPrimitiveRoot ζ k
i j : ℕ
hi : i < k
hj : j < k
H : ζ ^ i = ζ ^ j
inr : ∀ (this : ∀ ⦃i j : ℕ⦄ (hi : i < k) (hj : j < k) (H : ζ ^ i = ζ ^ j) (hij : i ≤ j), i = j) (hij : ¬i ≤ j), i = j
wlog : ∀ ⦃i j : ℕ⦄ (hi : i < k) (hj : j < k) (H : ζ ^ i = ζ ^ j) (hij : i ≤ j), i = j
⊢ i = j

Tactic:
wlog hij : i ≤ j generalizing i j
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
M : Type u_1
inst : CommMonoid M
k : ℕ
ζ : M
h : IsPrimitiveRoot ζ k
i j : ℕ
hi : i < k
hj : j < k
H : ζ ^ i = ζ ^ j
this : ∀ ⦃i j : ℕ⦄ (hi : i < k) (hj : j < k) (H : ζ ^ i = ζ ^ j) (hij : i ≤ j), i = j
hij : ¬i ≤ j
⊢ i = j

Tactic:
(this hj hi H.symm (le_of_not_ge hij)).symm

Premises used: le_of_not_ge, Eq.symm
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
M : Type u_1
inst : CommMonoid M
k : ℕ
ζ : M
h : IsPrimitiveRoot ζ k
i j : ℕ
hi : i < k
hj : j < k
H : ζ ^ i = ζ ^ j
this : ∀ ⦃i j : ℕ⦄ (hi : i < k) (hj : j < k) (H : ζ ^ i = ζ ^ j) (hij : i ≤ j), i = j
hij : ¬i ≤ j
⊢ i = j

Tactic:
exact (this hj hi H.symm (le_of_not_ge hij)).symm

Premises used: le_of_not_ge, Eq.symm
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
M : Type u_1
inst : CommMonoid M
k : ℕ
ζ : M
h : IsPrimitiveRoot ζ k
i j : ℕ
hi : i < k
hj : j < k
H : ζ ^ i = ζ ^ j
hij : i ≤ j
apply : j ≤ i
⊢ i = j

Tactic:
apply le_antisymm hij

Premises used: le_antisymm
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
M : Type u_1
inst : CommMonoid M
k : ℕ
ζ : M
h : IsPrimitiveRoot ζ k
i j : ℕ
hi : i < k
hj : j < k
H : ζ ^ i = ζ ^ j
hij : i ≤ j
rw : j - i = 0
⊢ j ≤ i

Tactic:
rw [← tsub_eq_zero_iff_le]

Premises used: tsub_eq_zero_iff_le
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
M : Type u_1
inst : CommMonoid M
k : ℕ
ζ : M
h : IsPrimitiveRoot ζ k
i j : ℕ
hi : i < k
hj : j < k
H : ζ ^ i = ζ ^ j
hij : i ≤ j
apply : k ∣ j - i
⊢ j - i = 0

Tactic:
apply Nat.eq_zero_of_dvd_of_lt _ (lt_of_le_of_lt tsub_le_self hj)

Premises used: lt_of_le_of_lt, tsub_le_self, Nat.eq_zero_of_dvd_of_lt
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
M : Type u_1
inst : CommMonoid M
k : ℕ
ζ : M
h : IsPrimitiveRoot ζ k
i j : ℕ
hi : i < k
hj : j < k
H : ζ ^ i = ζ ^ j
hij : i ≤ j
a : ζ ^ (j - i) = 1
⊢ k ∣ j - i

Tactic:
apply h.dvd_of_pow_eq_one

Premises used: IsPrimitiveRoot.dvd_of_pow_eq_one
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
M : Type u_1
inst : CommMonoid M
k : ℕ
ζ : M
h : IsPrimitiveRoot ζ k
i j : ℕ
hi : i < k
hj : j < k
H : ζ ^ i = ζ ^ j
hij : i ≤ j
a : ζ ^ (j - i) * ζ ^ i = 1 * ζ ^ i
a₁ : ζ ^ (j - i + i) = 1 * ζ ^ i
a₂ : ζ ^ j = 1 * ζ ^ i
a₃ : ζ ^ j = 1 * ζ ^ j
a₄ a₅ : ζ ^ j = ζ ^ j
⊢ ζ ^ (j - i) = 1

Tactic:
rw [← ((h.isUnit (Nat.ne_zero_of_lt hi)).pow i).mul_left_inj, ← pow_add,
    tsub_add_cancel_of_le hij, H, one_mul]

Premises used: pow_add, tsub_add_cancel_of_le, IsPrimitiveRoot.isUnit, IsUnit.pow, Nat.ne_zero_of_lt, IsUnit.mul_left_inj, one_mul
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
M : Type u_1
inst : CommMonoid M
⊢ IsPrimitiveRoot.{u_1} (M := M) 1 1

Tactic:
{ pow_eq_one := pow_one _
    dvd_of_pow_eq_one := fun _ _ ↦ one_dvd _ }

Premises used: IsPrimitiveRoot.mk, one_dvd, pow_one, OfNat.ofNat
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
M : Type u_1
inst : CommMonoid M
ζ : M
mp : IsPrimitiveRoot ζ 1 → ζ = 1
mpr : ζ = 1 → IsPrimitiveRoot ζ 1
⊢ IsPrimitiveRoot ζ 1 ↔ ζ = 1

Tactic:
constructor
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
M : Type u_1
inst : CommMonoid M
ζ : M
h : IsPrimitiveRoot ζ 1
mp : HPow.hPow (β := ℕ) ζ 1 = 1
mp₁ mp₂ : Eq.{u_1 + 1} (α := M) 1 1
⊢ ζ = 1

Tactic:
rw [← pow_one ζ, h.pow_eq_one]

Premises used: pow_one, IsPrimitiveRoot.pow_eq_one
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
M : Type u_1
inst : CommMonoid M
⊢ IsPrimitiveRoot.{u_1} (M := M) 1 1

Tactic:
one

Premises used: IsPrimitiveRoot.one
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
M : Type u_1
inst : CommMonoid M
⊢ IsPrimitiveRoot.{u_1} (M := M) 1 1

Tactic:
exact one

Premises used: IsPrimitiveRoot.one
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
k : ℕ
M : Type u_7
B : Type u_8
inst : CommMonoid M
inst_1 : SetLike B M
inst_2 : SubmonoidClass B M
N : B
ζ : ↥N
simp_rw : ((↑ζ : M) ^ k = 1 ∧ ∀ (l : ℕ), (↑ζ : M) ^ l = 1 → k ∣ l) ↔ ζ ^ k = 1 ∧ ∀ (l : ℕ), ζ ^ l = 1 → k ∣ l
⊢ IsPrimitiveRoot (↑ζ : M) k ↔ IsPrimitiveRoot ζ k

Tactic:
simp_rw [iff_def]

Premises used: IsPrimitiveRoot.iff_def