Skip to content
This repository was archived by the owner on Jul 24, 2024. It is now read-only.

Commit 64289fe

Browse files
committed
chore(group_theory/order_of_element): fix weird lemma name (#10245)
1 parent 10d3d25 commit 64289fe

File tree

1 file changed

+1
-1
lines changed

1 file changed

+1
-1
lines changed

src/group_theory/order_of_element.lean

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -119,7 +119,7 @@ by rwa [order_of, minimal_period, dif_neg]
119119
⟨λ h H, (order_of_pos' H).ne' h, order_of_eq_zero⟩
120120

121121
@[to_additive nsmul_ne_zero_of_lt_add_order_of']
122-
lemma pow_eq_one_of_lt_order_of' (n0 : n ≠ 0) (h : n < order_of x) : x ^ n ≠ 1 :=
122+
lemma pow_ne_one_of_lt_order_of' (n0 : n ≠ 0) (h : n < order_of x) : x ^ n ≠ 1 :=
123123
λ j, not_is_periodic_pt_of_pos_of_lt_minimal_period n0 h
124124
((is_periodic_pt_mul_iff_pow_eq_one x).mpr j)
125125

0 commit comments

Comments
 (0)