chore(Algebra/GroupPower/Order): Fix "See also" comment (#9384)

Reported by Alex [here](d61c95e)
leanprover-community · Jan 1, 2024 · 4ae4613 · 4ae4613
1 parent 5683185
commit 4ae4613
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/Mathlib/Algebra/GroupPower/Order.lean b/Mathlib/Algebra/GroupPower/Order.lean
@@ -126,7 +126,7 @@ theorem pow_lt_pow_left (h : x < y) (hx : 0 ≤ x) : ∀ {n : ℕ}, n ≠ 0 →
       mul_lt_mul_of_le_of_le' (pow_le_pow_left hx h.le _) h (pow_pos (hx.trans_lt h) _) hx
 #align pow_lt_pow_of_lt_left pow_lt_pow_left
 
-/-- See also `pow_left_strictMonoOn`. -/
+/-- See also `pow_left_strictMono` and `Nat.pow_left_strictMono`. -/
 lemma pow_left_strictMonoOn (hn : n ≠ 0) : StrictMonoOn (· ^ n : R → R) (Set.Ici 0) :=
   fun _a ha _b _ hab ↦ pow_lt_pow_left hab ha hn
 #align strict_mono_on_pow pow_left_strictMonoOn