M : Type ?u.2707095
N : Type ?u.2707098
G : Type u_1
R : Type ?u.2707104
S : Type ?u.2707107
F : Type ?u.2707110
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
inst✝ : DivisionCommMonoid G
k l : ℕ
ζ : G
⊢ IsPrimitiveRoot ζ⁻¹ k → IsPrimitiveRoot ζ k
M : Type ?u.2707095
N : Type ?u.2707098
G : Type u_1
R : Type ?u.2707104
S : Type ?u.2707107
F : Type ?u.2707110
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
inst✝ : DivisionCommMonoid G
k l : ℕ
ζ : G
⊢ IsPrimitiveRoot ζ⁻¹ k ↔ IsPrimitiveRoot ζ k
refine' ⟨_, fun h => inv h⟩
M : Type ?u.2707095
N : Type ?u.2707098
G : Type u_1
R : Type ?u.2707104
S : Type ?u.2707107
F : Type ?u.2707110
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
inst✝ : DivisionCommMonoid G
k l : ℕ
ζ : G
h : IsPrimitiveRoot ζ⁻¹ k
⊢ IsPrimitiveRoot ζ k
M : Type ?u.2707095
N : Type ?u.2707098
G : Type u_1
R : Type ?u.2707104
S : Type ?u.2707107
F : Type ?u.2707110
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
inst✝ : DivisionCommMonoid G
k l : ℕ
ζ : G
⊢ IsPrimitiveRoot ζ⁻¹ k → IsPrimitiveRoot ζ k
intro h
M : Type ?u.2707095
N : Type ?u.2707098
G : Type u_1
R : Type ?u.2707104
S : Type ?u.2707107
F : Type ?u.2707110
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
inst✝ : DivisionCommMonoid G
k l : ℕ
ζ : G
h : IsPrimitiveRoot ζ⁻¹ k
⊢ IsPrimitiveRoot ζ⁻¹⁻¹ k
M : Type ?u.2707095
N : Type ?u.2707098
G : Type u_1
R : Type ?u.2707104
S : Type ?u.2707107
F : Type ?u.2707110
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
inst✝ : DivisionCommMonoid G
k l : ℕ
ζ : G
h : IsPrimitiveRoot ζ⁻¹ k
⊢ IsPrimitiveRoot ζ k
rw [← inv_inv ζ]
no goals
M : Type ?u.2707095
N : Type ?u.2707098
G : Type u_1
R : Type ?u.2707104
S : Type ?u.2707107
F : Type ?u.2707110
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
inst✝ : DivisionCommMonoid G
k l : ℕ
ζ : G
h : IsPrimitiveRoot ζ⁻¹ k
⊢ IsPrimitiveRoot ζ⁻¹⁻¹ k
exact inv h