Theorem: ModularCyclotomicCharacter.ext (AntLorentz/CyclotomicCharacter.lean)

State before:
L : Type u
inst✝³ : Field L
n : ℕ+
G : Type u_1
inst✝² : Group G
inst✝¹ : Fintype G
inst✝ : IsCyclic G
d : ℕ
a b : ZMod d
hGcard : Fintype.card G = d
h : ∀ (t : G), t ^ ZMod.val a = t ^ ZMod.val b
⊢ a = b
Tactic:
obtain ⟨g, hg⟩ := IsCyclic.exists_generator (α := G)
State after:
case intro
L : Type u
inst✝³ : Field L
n : ℕ+
G : Type u_1
inst✝² : Group G
inst✝¹ : Fintype G
inst✝ : IsCyclic G
d : ℕ
a b : ZMod d
hGcard : Fintype.card G = d
h : ∀ (t : G), t ^ ZMod.val a = t ^ ZMod.val b
g : G
hg : ∀ (x : G), x ∈ Subgroup.zpowers g
⊢ a = b

State before:
case intro
L : Type u
inst✝³ : Field L
n : ℕ+
G : Type u_1
inst✝² : Group G
inst✝¹ : Fintype G
inst✝ : IsCyclic G
d : ℕ
a b : ZMod d
hGcard : Fintype.card G = d
h : ∀ (t : G), t ^ ZMod.val a = t ^ ZMod.val b
g : G
hg : ∀ (x : G), x ∈ Subgroup.zpowers g
⊢ a = b
Tactic:
have hgord := orderOf_eq_card_of_forall_mem_zpowers hg
State after:
case intro
L : Type u
inst✝³ : Field L
n : ℕ+
G : Type u_1
inst✝² : Group G
inst✝¹ : Fintype G
inst✝ : IsCyclic G
d : ℕ
a b : ZMod d
hGcard : Fintype.card G = d
h : ∀ (t : G), t ^ ZMod.val a = t ^ ZMod.val b
g : G
hg : ∀ (x : G), x ∈ Subgroup.zpowers g
hgord : orderOf g = Fintype.card G
⊢ a = b

State before:
case intro
L : Type u
inst✝³ : Field L
n : ℕ+
G : Type u_1
inst✝² : Group G
inst✝¹ : Fintype G
inst✝ : IsCyclic G
d : ℕ
a b : ZMod d
hGcard : Fintype.card G = d
h : ∀ (t : G), t ^ ZMod.val a = t ^ ZMod.val b
g : G
hg : ∀ (x : G), x ∈ Subgroup.zpowers g
hgord : orderOf g = Fintype.card G
⊢ a = b
Tactic:
specialize h g
State after:
case intro
L : Type u
inst✝³ : Field L
n : ℕ+
G : Type u_1
inst✝² : Group G
inst✝¹ : Fintype G
inst✝ : IsCyclic G
d : ℕ
a b : ZMod d
hGcard : Fintype.card G = d
g : G
hg : ∀ (x : G), x ∈ Subgroup.zpowers g
hgord : orderOf g = Fintype.card G
h : g ^ ZMod.val a = g ^ ZMod.val b
⊢ a = b

State before:
case intro
L : Type u
inst✝³ : Field L
n : ℕ+
G : Type u_1
inst✝² : Group G
inst✝¹ : Fintype G
inst✝ : IsCyclic G
d : ℕ
a b : ZMod d
hGcard : Fintype.card G = d
g : G
hg : ∀ (x : G), x ∈ Subgroup.zpowers g
hgord : orderOf g = Fintype.card G
h : g ^ ZMod.val a = g ^ ZMod.val b
⊢ a = b
Tactic:
rw [pow_eq_pow_iff_modEq, hgord, hGcard, ← ZMod.nat_cast_eq_nat_cast_iff] at h
State after:
case intro
L : Type u
inst✝³ : Field L
n : ℕ+
G : Type u_1
inst✝² : Group G
inst✝¹ : Fintype G
inst✝ : IsCyclic G
d : ℕ
a b : ZMod d
hGcard : Fintype.card G = d
g : G
hg : ∀ (x : G), x ∈ Subgroup.zpowers g
hgord : orderOf g = Fintype.card G
h : ↑(ZMod.val a) = ↑(ZMod.val b)
⊢ a = b

State before:
case intro
L : Type u
inst✝³ : Field L
n : ℕ+
G : Type u_1
inst✝² : Group G
inst✝¹ : Fintype G
inst✝ : IsCyclic G
d : ℕ
a b : ZMod d
hGcard : Fintype.card G = d
g : G
hg : ∀ (x : G), x ∈ Subgroup.zpowers g
hgord : orderOf g = Fintype.card G
h : ↑(ZMod.val a) = ↑(ZMod.val b)
⊢ a = b
Tactic:
subst hGcard
State after:
case intro
L : Type u
inst✝³ : Field L
n : ℕ+
G : Type u_1
inst✝² : Group G
inst✝¹ : Fintype G
inst✝ : IsCyclic G
g : G
hg : ∀ (x : G), x ∈ Subgroup.zpowers g
hgord : orderOf g = Fintype.card G
a b : ZMod (Fintype.card G)
h : ↑(ZMod.val a) = ↑(ZMod.val b)
⊢ a = b

State before:
case intro
L : Type u
inst✝³ : Field L
n : ℕ+
G : Type u_1
inst✝² : Group G
inst✝¹ : Fintype G
inst✝ : IsCyclic G
g : G
hg : ∀ (x : G), x ∈ Subgroup.zpowers g
hgord : orderOf g = Fintype.card G
a b : ZMod (Fintype.card G)
h : ↑(ZMod.val a) = ↑(ZMod.val b)
⊢ a = b
Tactic:
simpa [ZMod.nat_cast_val, ZMod.cast_id'] using h
State after:
no goals