c ^ n tends to 0 in complexes

Stream: Is there code for X?

[Bhavik Mehta]

Do we have this?

import Mathlib.Analysis.Complex.Basic

open Filter Topology

example {c : ℂ} (hc : ‖c‖ < 1) : Tendsto (c ^ ·) atTop (𝓝 0) := by
  sorry

I presume it also works for normed fields or something, but I'd be happy with any reasonable version of the above - loogle and exact? and leansearch are all failing to find it for me

[Bhavik Mehta]

Ah, here we go:

example {E : Type*} [NormedDivisionRing E]
    {c : E} (hc : ‖c‖ < 1) : Tendsto (c ^ ·) atTop (𝓝 0) := by
  rw [tendsto_zero_iff_norm_tendsto_zero]
  simpa

I'm still slightly surprised this wasn't in mathlib already, especially since we have docs#tendsto_pow_atTop_nhds_zero_iff

[Etienne Marion]

It's docs#tendsto_pow_atTop_nhds_zero_of_norm_lt_one I think?

[Etienne Marion]

(deleted)

[Etienne Marion]

@loogle ‖_‖ < 1, Filter.Tendsto

[loogle]

:search: tendsto_pow_atTop_nhds_zero_of_norm_lt_one, CStarAlgebra.tendsto_mul_right_of_forall_nonneg_tendsto, and 1 more

[Bhavik Mehta]

Ah, so it is. Thank you!

[Bhavik Mehta]

I searched nhds, Filter.Tendsto, Filter.atTop, "pow" and got a ton of unhelpful things