[Merged by Bors] - chore(Analysis/SpecificLimits/* and others): rename _0 -> _zero, _1 -> _one

[MichaelStollBayreuth]

See here on Zulip.

This PR changes a bunch of names containing nhds_0 or/and lt_1 to nhds_zero or/and lt_one.

---

[kbuzzard]

This looks fine to me! Thanks a lot for doing it!

[kbuzzard]

I don't know enough about @[deprecated]: can you confirm that you don't need to put the Real namespace for this line to be effective? (in contrast to #align which does need them)

Thanks a lot for taking care of the #aligns and @[deprecated] by the way.

[MichaelStollBayreuth]

I think it works (at least I got a bunch of warnings that stuff is deprecated).

[kbuzzard]

Yikes, github making our life harder with this diff. @alexjbest can you use Leaff to confirm that this PR only does what it claims to do? Can you even check the @[deprecated] stuff does what it's supposed to do?

[linesthatinterlace]

It looks fine to me from a visual inspection.

[linesthatinterlace]

Frankly you could leave out the deprecated lines but it's probably kinder to keep them in I guess.)

[MichaelStollBayreuth]

I imagine these results are likely to be used in downstream projects, and there it is nice to be told automatically after updating Mathlib that the names are now deprecated, with the offer of fixing them (rather than getting an "unknown identifier" error and having to consult the change log).

[linesthatinterlace]

As I say, it is kinder - I like that we have the option and I like that you've done it.

[adri326]

A clever grep search yields a few other theorem names that could receive the same treatment.
Here are the ripgrep commands I used:

# Clean output, whitelist-based
rg '^(?:protected\s+)?(?:theorem|lemma)\s+[\w_]+?(?:ge|lt|le|gt|eq|ne|at|tendsto|nhds|exp)(?<!image|[aA]lt|triangle)_?[0-5](?![0-9])' --pcre2

# More noisy, blacklist-based, but catches a few exceptions to the common patterns
rg '^(?:protected\s+)?(?:theorem|lemma)\s+[\w_]+(?<!bit|bitm|div|aleph|image|deriv|L|C|C_|[aA]ux|lem|sym|append|node|fold[lr]|[fF]in|vecAlt|Gamma|T)[0-3](?![0-9]|Space|_separation)' --pcre2

Mathlib/Analysis/ODE/Gronwall.lean

• gronwallBound_of_K_ne_0

Mathlib/Logic/Function/Iterate.lean

• involutive_iff_iter_2_eq_id

Mathlib/RingTheory/Polynomial/Bernstein.lean

• eval_at_0
• eval_at_1
• iterate_derivative_at_0_eq_zero_of_lt
• iterate_derivative_succ_at_0_eq_zero
• iterate_derivative_at_0
• iterate_derivative_at_0_ne_zero
• iterate_derivative_at_1_eq_zero_of_lt
• iterate_derivative_at_1
• iterate_derivative_at_1_ne_zero

Mathlib/Algebra/GroupWithZero/Basic.lean

• zero_ne_one_or_forall_eq_0

Mathlib/Topology/MetricSpace/Cauchy.lean

• cauchySeq_of_le_tendsto_0'
• cauchySeq_of_le_tendsto_0
• cauchySeq_iff_le_tendsto_0

Mathlib/Topology/Instances/ENNReal.lean

• tendsto_iff_edist_tendsto_0

Mathlib/Data/Set/Pointwise/Interval.lean

• inv_Ioo_0_left

Mathlib/Analysis/Convex/Normed.lean

• convexHull_exists_dist_ge2

Mathlib/Analysis/SpecialFunctions/Log/Deriv.lean

• hasSum_pow_div_log_of_abs_lt_1
• hasSum_log_sub_log_of_abs_lt_1

Mathlib/Analysis/SpecialFunctions/Exp.lean

• tendsto_exp_neg_atTop_nhds_0
• tendsto_exp_nhds_0_nhds_1
• tendsto_pow_mul_exp_neg_atTop_nhds_0

Mathlib/LinearAlgebra/Eigenspace/Minpoly.lean

• eigenspace_aeval_polynomial_degree_1

Mathlib/Analysis/SpecificLimits/Normed.lean

• lots of them

Mathlib/Analysis/SpecificLimits/Basic.lean

• also lots of them

Mathlib/Data/Complex/Exponential.lean

• exp_1_approx_succ_eq

Mathlib/RingTheory/UniqueFactorizationDomain.lean

• factors_0

Mathlib/AlgebraicTopology/ExtraDegeneracy.lean

• shiftFun_0

[MichaelStollBayreuth]

@adri326 I'll leave cleaning up the remaining ones to somebody else. This PR was enough work for me 😄

[MichaelStollBayreuth]

Polynomial.C_0 and Polynomial.C_1 should probably also be renamed.

[semorrison]

bors merge

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Check all files imported
• Lint style