M : Type ?u.3884431
N : Type ?u.3884434
G : Type ?u.3884437
R : Type u_1
S : Type u_2
F : Type ?u.3884446
inst✝⁶ : CommMonoid M
inst✝⁵ : CommMonoid N
inst✝⁴ : DivisionCommMonoid G
k l : ℕ
inst✝³ : CommRing S
inst✝² : IsDomain S
μ : S
n : ℕ+
hμ : IsPrimitiveRoot μ ↑n
inst✝¹ : CommRing R
inst✝ : Algebra R S
f : S ≃ₐ[R] S
⊢ μ ^ ZMod.val ↑(Exists.choose (_ : ∃ m, ↑f ↑↑(toRootsOfUnity hμ) = ↑↑(toRootsOfUnity hμ) ^ m)) = ↑f μ
M : Type ?u.3884431
N : Type ?u.3884434
G : Type ?u.3884437
R : Type u_1
S : Type u_2
F : Type ?u.3884446
inst✝⁶ : CommMonoid M
inst✝⁵ : CommMonoid N
inst✝⁴ : DivisionCommMonoid G
k l : ℕ
inst✝³ : CommRing S
inst✝² : IsDomain S
μ : S
n : ℕ+
hμ : IsPrimitiveRoot μ ↑n
inst✝¹ : CommRing R
inst✝ : Algebra R S
f : S ≃ₐ[R] S
⊢ μ ^ ZMod.val ↑(↑(autToPow R hμ) f) = ↑f μ
rw [IsPrimitiveRoot.coe_autToPow_apply]
M : Type ?u.3884431
N : Type ?u.3884434
G : Type ?u.3884437
R : Type u_1
S : Type u_2
F : Type ?u.3884446
inst✝⁶ : CommMonoid M
inst✝⁵ : CommMonoid N
inst✝⁴ : DivisionCommMonoid G
k l : ℕ
inst✝³ : CommRing S
inst✝² : IsDomain S
μ : S
n : ℕ+
hμ : IsPrimitiveRoot μ ↑n
inst✝¹ : CommRing R
inst✝ : Algebra R S
f : S ≃ₐ[R] S
h : ∃ m, ↑f ↑↑(toRootsOfUnity hμ) = ↑↑(toRootsOfUnity hμ) ^ m
⊢ μ ^ ZMod.val ↑(Exists.choose h) = ↑f μ
M : Type ?u.3884431
N : Type ?u.3884434
G : Type ?u.3884437
R : Type u_1
S : Type u_2
F : Type ?u.3884446
inst✝⁶ : CommMonoid M
inst✝⁵ : CommMonoid N
inst✝⁴ : DivisionCommMonoid G
k l : ℕ
inst✝³ : CommRing S
inst✝² : IsDomain S
μ : S
n : ℕ+
hμ : IsPrimitiveRoot μ ↑n
inst✝¹ : CommRing R
inst✝ : Algebra R S
f : S ≃ₐ[R] S
⊢ μ ^ ZMod.val ↑(Exists.choose (_ : ∃ m, ↑f ↑↑(toRootsOfUnity hμ) = ↑↑(toRootsOfUnity hμ) ^ m)) = ↑f μ
generalize_proofs h
M : Type ?u.3884431
N : Type ?u.3884434
G : Type ?u.3884437
R : Type u_1
S : Type u_2
F : Type ?u.3884446
inst✝⁶ : CommMonoid M
inst✝⁵ : CommMonoid N
inst✝⁴ : DivisionCommMonoid G
k l : ℕ
inst✝³ : CommRing S
inst✝² : IsDomain S
μ : S
n : ℕ+
hμ : IsPrimitiveRoot μ ↑n
inst✝¹ : CommRing R
inst✝ : Algebra R S
f : S ≃ₐ[R] S
h : ∃ m, ↑f ↑↑(toRootsOfUnity hμ) = ↑↑(toRootsOfUnity hμ) ^ m
this : ↑f ↑↑(toRootsOfUnity hμ) = ↑↑(toRootsOfUnity hμ) ^ Exists.choose h
⊢ μ ^ ZMod.val ↑(Exists.choose h) = ↑f μ
M : Type ?u.3884431
N : Type ?u.3884434
G : Type ?u.3884437
R : Type u_1
S : Type u_2
F : Type ?u.3884446
inst✝⁶ : CommMonoid M
inst✝⁵ : CommMonoid N
inst✝⁴ : DivisionCommMonoid G
k l : ℕ
inst✝³ : CommRing S
inst✝² : IsDomain S
μ : S
n : ℕ+
hμ : IsPrimitiveRoot μ ↑n
inst✝¹ : CommRing R
inst✝ : Algebra R S
f : S ≃ₐ[R] S
h : ∃ m, ↑f ↑↑(toRootsOfUnity hμ) = ↑↑(toRootsOfUnity hμ) ^ m
⊢ μ ^ ZMod.val ↑(Exists.choose h) = ↑f μ
have := h.choose_spec
M : Type ?u.3884431
N : Type ?u.3884434
G : Type ?u.3884437
R : Type u_1
S : Type u_2
F : Type ?u.3884446
inst✝⁶ : CommMonoid M
inst✝⁵ : CommMonoid N
inst✝⁴ : DivisionCommMonoid G
k l : ℕ
inst✝³ : CommRing S
inst✝² : IsDomain S
μ : S
n : ℕ+
hμ : IsPrimitiveRoot μ ↑n
inst✝¹ : CommRing R
inst✝ : Algebra R S
f : S ≃ₐ[R] S
h : ∃ m, ↑f ↑↑(toRootsOfUnity hμ) = ↑↑(toRootsOfUnity hμ) ^ m
this : ↑f ↑↑(toRootsOfUnity hμ) = ↑↑(toRootsOfUnity hμ) ^ Exists.choose h
⊢ μ ^ ZMod.val ↑(Exists.choose h) = ↑f μ
M : Type ?u.3884431
N : Type ?u.3884434
G : Type ?u.3884437
R : Type u_1
S : Type u_2
F : Type ?u.3884446
inst✝⁶ : CommMonoid M
inst✝⁵ : CommMonoid N
inst✝⁴ : DivisionCommMonoid G
k l : ℕ
inst✝³ : CommRing S
inst✝² : IsDomain S
μ : S
n : ℕ+
hμ : IsPrimitiveRoot μ ↑n
inst✝¹ : CommRing R
inst✝ : Algebra R S
f : S ≃ₐ[R] S
h : ∃ m, ↑f ↑↑(toRootsOfUnity hμ) = ↑↑(toRootsOfUnity hμ) ^ m
this : ↑f ↑↑(toRootsOfUnity hμ) = ↑↑(toRootsOfUnity hμ) ^ Exists.choose h
⊢ μ ^ ZMod.val ↑(Exists.choose h) = ↑f μ
dsimp only [AlgEquiv.toAlgHom_eq_coe, AlgEquiv.coe_algHom] at this
M : Type ?u.3884431
N : Type ?u.3884434
G : Type ?u.3884437
R : Type u_1
S : Type u_2
F : Type ?u.3884446
inst✝⁶ : CommMonoid M
inst✝⁵ : CommMonoid N
inst✝⁴ : DivisionCommMonoid G
k l : ℕ
inst✝³ : CommRing S
inst✝² : IsDomain S
μ : S
n : ℕ+
hμ : IsPrimitiveRoot μ ↑n
inst✝¹ : CommRing R
inst✝ : Algebra R S
f : S ≃ₐ[R] S
h : ∃ m, ↑f ↑↑(toRootsOfUnity hμ) = ↑↑(toRootsOfUnity hμ) ^ m
this : ↑f ↑↑(toRootsOfUnity hμ) = ↑↑(toRootsOfUnity hμ) ^ Exists.choose h
⊢ ↑↑(toRootsOfUnity hμ) ^ ZMod.val ↑(Exists.choose h) = ↑↑(toRootsOfUnity hμ) ^ Exists.choose h
M : Type ?u.3884431
N : Type ?u.3884434
G : Type ?u.3884437
R : Type u_1
S : Type u_2
F : Type ?u.3884446
inst✝⁶ : CommMonoid M
inst✝⁵ : CommMonoid N
inst✝⁴ : DivisionCommMonoid G
k l : ℕ
inst✝³ : CommRing S
inst✝² : IsDomain S
μ : S
n : ℕ+
hμ : IsPrimitiveRoot μ ↑n
inst✝¹ : CommRing R
inst✝ : Algebra R S
f : S ≃ₐ[R] S
h : ∃ m, ↑f ↑↑(toRootsOfUnity hμ) = ↑↑(toRootsOfUnity hμ) ^ m
this : ↑f ↑↑(toRootsOfUnity hμ) = ↑↑(toRootsOfUnity hμ) ^ Exists.choose h
⊢ μ ^ ZMod.val ↑(Exists.choose h) = ↑f μ
refine' (_ : ((hμ.toRootsOfUnity : Sˣ) : S) ^ _ = _).trans this.symm
M : Type ?u.3884431
N : Type ?u.3884434
G : Type ?u.3884437
R : Type u_1
S : Type u_2
F : Type ?u.3884446
inst✝⁶ : CommMonoid M
inst✝⁵ : CommMonoid N
inst✝⁴ : DivisionCommMonoid G
k l : ℕ
inst✝³ : CommRing S
inst✝² : IsDomain S
μ : S
n : ℕ+
hμ : IsPrimitiveRoot μ ↑n
inst✝¹ : CommRing R
inst✝ : Algebra R S
f : S ≃ₐ[R] S
h : ∃ m, ↑f ↑↑(toRootsOfUnity hμ) = ↑↑(toRootsOfUnity hμ) ^ m
this : ↑f ↑↑(toRootsOfUnity hμ) = ↑↑(toRootsOfUnity hμ) ^ Exists.choose h
⊢ ↑↑(toRootsOfUnity hμ ^ ZMod.val ↑(Exists.choose h)) = ↑↑(toRootsOfUnity hμ ^ Exists.choose h)
M : Type ?u.3884431
N : Type ?u.3884434
G : Type ?u.3884437
R : Type u_1
S : Type u_2
F : Type ?u.3884446
inst✝⁶ : CommMonoid M
inst✝⁵ : CommMonoid N
inst✝⁴ : DivisionCommMonoid G
k l : ℕ
inst✝³ : CommRing S
inst✝² : IsDomain S
μ : S
n : ℕ+
hμ : IsPrimitiveRoot μ ↑n
inst✝¹ : CommRing R
inst✝ : Algebra R S
f : S ≃ₐ[R] S
h : ∃ m, ↑f ↑↑(toRootsOfUnity hμ) = ↑↑(toRootsOfUnity hμ) ^ m
this : ↑f ↑↑(toRootsOfUnity hμ) = ↑↑(toRootsOfUnity hμ) ^ Exists.choose h
⊢ ↑↑(toRootsOfUnity hμ) ^ ZMod.val ↑(Exists.choose h) = ↑↑(toRootsOfUnity hμ) ^ Exists.choose h
rw [← rootsOfUnity.coe_pow, ← rootsOfUnity.coe_pow]
case e_self.e_self
M : Type ?u.3884431
N : Type ?u.3884434
G : Type ?u.3884437
R : Type u_1
S : Type u_2
F : Type ?u.3884446
inst✝⁶ : CommMonoid M
inst✝⁵ : CommMonoid N
inst✝⁴ : DivisionCommMonoid G
k l : ℕ
inst✝³ : CommRing S
inst✝² : IsDomain S
μ : S
n : ℕ+
hμ : IsPrimitiveRoot μ ↑n
inst✝¹ : CommRing R
inst✝ : Algebra R S
f : S ≃ₐ[R] S
h : ∃ m, ↑f ↑↑(toRootsOfUnity hμ) = ↑↑(toRootsOfUnity hμ) ^ m
this : ↑f ↑↑(toRootsOfUnity hμ) = ↑↑(toRootsOfUnity hμ) ^ Exists.choose h
⊢ toRootsOfUnity hμ ^ ZMod.val ↑(Exists.choose h) = toRootsOfUnity hμ ^ Exists.choose h
M : Type ?u.3884431
N : Type ?u.3884434
G : Type ?u.3884437
R : Type u_1
S : Type u_2
F : Type ?u.3884446
inst✝⁶ : CommMonoid M
inst✝⁵ : CommMonoid N
inst✝⁴ : DivisionCommMonoid G
k l : ℕ
inst✝³ : CommRing S
inst✝² : IsDomain S
μ : S
n : ℕ+
hμ : IsPrimitiveRoot μ ↑n
inst✝¹ : CommRing R
inst✝ : Algebra R S
f : S ≃ₐ[R] S
h : ∃ m, ↑f ↑↑(toRootsOfUnity hμ) = ↑↑(toRootsOfUnity hμ) ^ m
this : ↑f ↑↑(toRootsOfUnity hμ) = ↑↑(toRootsOfUnity hμ) ^ Exists.choose h
⊢ ↑↑(toRootsOfUnity hμ ^ ZMod.val ↑(Exists.choose h)) = ↑↑(toRootsOfUnity hμ ^ Exists.choose h)
congr 2
case e_self.e_self
M : Type ?u.3884431
N : Type ?u.3884434
G : Type ?u.3884437
R : Type u_1
S : Type u_2
F : Type ?u.3884446
inst✝⁶ : CommMonoid M
inst✝⁵ : CommMonoid N
inst✝⁴ : DivisionCommMonoid G
k l : ℕ
inst✝³ : CommRing S
inst✝² : IsDomain S
μ : S
n : ℕ+
hμ : IsPrimitiveRoot μ ↑n
inst✝¹ : CommRing R
inst✝ : Algebra R S
f : S ≃ₐ[R] S
h : ∃ m, ↑f ↑↑(toRootsOfUnity hμ) = ↑↑(toRootsOfUnity hμ) ^ m
this : ↑f ↑↑(toRootsOfUnity hμ) = ↑↑(toRootsOfUnity hμ) ^ Exists.choose h
⊢ Exists.choose h % orderOf μ ≡ Exists.choose h [MOD orderOf ↑↑(toRootsOfUnity hμ)]
case e_self.e_self
M : Type ?u.3884431
N : Type ?u.3884434
G : Type ?u.3884437
R : Type u_1
S : Type u_2
F : Type ?u.3884446
inst✝⁶ : CommMonoid M
inst✝⁵ : CommMonoid N
inst✝⁴ : DivisionCommMonoid G
k l : ℕ
inst✝³ : CommRing S
inst✝² : IsDomain S
μ : S
n : ℕ+
hμ : IsPrimitiveRoot μ ↑n
inst✝¹ : CommRing R
inst✝ : Algebra R S
f : S ≃ₐ[R] S
h : ∃ m, ↑f ↑↑(toRootsOfUnity hμ) = ↑↑(toRootsOfUnity hμ) ^ m
this : ↑f ↑↑(toRootsOfUnity hμ) = ↑↑(toRootsOfUnity hμ) ^ Exists.choose h
⊢ toRootsOfUnity hμ ^ ZMod.val ↑(Exists.choose h) = toRootsOfUnity hμ ^ Exists.choose h
rw [pow_eq_pow_iff_modEq, ZMod.val_nat_cast, hμ.eq_orderOf, ← orderOf_subgroup, ← orderOf_units]
no goals
case e_self.e_self
M : Type ?u.3884431
N : Type ?u.3884434
G : Type ?u.3884437
R : Type u_1
S : Type u_2
F : Type ?u.3884446
inst✝⁶ : CommMonoid M
inst✝⁵ : CommMonoid N
inst✝⁴ : DivisionCommMonoid G
k l : ℕ
inst✝³ : CommRing S
inst✝² : IsDomain S
μ : S
n : ℕ+
hμ : IsPrimitiveRoot μ ↑n
inst✝¹ : CommRing R
inst✝ : Algebra R S
f : S ≃ₐ[R] S
h : ∃ m, ↑f ↑↑(toRootsOfUnity hμ) = ↑↑(toRootsOfUnity hμ) ^ m
this : ↑f ↑↑(toRootsOfUnity hμ) = ↑↑(toRootsOfUnity hμ) ^ Exists.choose h
⊢ Exists.choose h % orderOf μ ≡ Exists.choose h [MOD orderOf ↑↑(toRootsOfUnity hμ)]
exact Nat.mod_modEq _ _