case h
G : Type u
A : Type v
x✝ y : G
a b : A
n m : ℕ
inst✝² : Monoid G
inst✝¹ : AddMonoid A
H : Type u_1
inst✝ : Monoid H
ψ : G →* H
x : G
⊢ ↑ψ x ^ orderOf x = 1
G : Type u
A : Type v
x✝ y : G
a b : A
n m : ℕ
inst✝² : Monoid G
inst✝¹ : AddMonoid A
H : Type u_1
inst✝ : Monoid H
ψ : G →* H
x : G
⊢ orderOf (↑ψ x) ∣ orderOf x
apply orderOf_dvd_of_pow_eq_one
case h
G : Type u
A : Type v
x✝ y : G
a b : A
n m : ℕ
inst✝² : Monoid G
inst✝¹ : AddMonoid A
H : Type u_1
inst✝ : Monoid H
ψ : G →* H
x : G
⊢ ↑ψ 1 = 1
case h
G : Type u
A : Type v
x✝ y : G
a b : A
n m : ℕ
inst✝² : Monoid G
inst✝¹ : AddMonoid A
H : Type u_1
inst✝ : Monoid H
ψ : G →* H
x : G
⊢ ↑ψ x ^ orderOf x = 1
rw [← map_pow, pow_orderOf_eq_one]
no goals
case h
G : Type u
A : Type v
x✝ y : G
a b : A
n m : ℕ
inst✝² : Monoid G
inst✝¹ : AddMonoid A
H : Type u_1
inst✝ : Monoid H
ψ : G →* H
x : G
⊢ ↑ψ 1 = 1
apply map_one