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

Commit e6c6dfd

Browse files
committed
chore(analysis/special_functions): correct typo (#16280)
1 parent 879155b commit e6c6dfd

File tree

1 file changed

+1
-1
lines changed

1 file changed

+1
-1
lines changed

src/analysis/special_functions/pow.lean

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1069,7 +1069,7 @@ lemma tendsto_log_div_rpow_nhds_zero {r : ℝ} (hr : r < 0) :
10691069
tendsto (λ x, log x / x ^ r) (𝓝[>] 0) (𝓝 0) :=
10701070
(is_o_log_rpow_nhds_zero hr).tendsto_div_nhds_zero
10711071

1072-
lemma tensdto_log_mul_rpow_nhds_zero {r : ℝ} (hr : 0 < r) :
1072+
lemma tendsto_log_mul_rpow_nhds_zero {r : ℝ} (hr : 0 < r) :
10731073
tendsto (λ x, log x * x ^ r) (𝓝[>] 0) (𝓝 0) :=
10741074
(tendsto_log_div_rpow_nhds_zero $ neg_lt_zero.2 hr).congr' $
10751075
eventually_mem_nhds_within.mono $ λ x hx, by rw [rpow_neg hx.out.le, div_inv_eq_mul]

0 commit comments

Comments
 (0)