Commit 2024-01-31 21:36 4e65ea9e

View on Github →

chore(Analysis/SpecificLimits/* and others): rename _0 -> _zero, _1 -> _one (#10077) 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.

Estimated changes

Modified Mathlib/Analysis/Analytic/Basic.lean

Modified Mathlib/Analysis/Analytic/Constructions.lean

Modified Mathlib/Analysis/Asymptotics/Asymptotics.lean

deleted theorem Asymptotics.IsBigOWith.right_le_add_of_lt_1

added theorem Asymptotics.IsBigOWith.right_le_add_of_lt_one

deleted theorem Asymptotics.IsBigOWith.right_le_sub_of_lt_1

added theorem Asymptotics.IsBigOWith.right_le_sub_of_lt_one

Modified Mathlib/Analysis/Calculus/InverseFunctionTheorem/ApproximatesLinearOn.lean

Modified Mathlib/Analysis/Calculus/TangentCone.lean

Modified Mathlib/Analysis/InnerProductSpace/Projection.lean

Modified Mathlib/Analysis/NormedSpace/Banach.lean

Modified Mathlib/Analysis/NormedSpace/Spectrum.lean

Modified Mathlib/Analysis/NormedSpace/Units.lean

Modified Mathlib/Analysis/PSeries.lean

Modified Mathlib/Analysis/SpecialFunctions/Bernstein.lean

Modified Mathlib/Analysis/SpecialFunctions/Complex/LogBounds.lean

Modified Mathlib/Analysis/SpecialFunctions/Exp.lean

deleted theorem Real.tendsto_exp_neg_atTop_nhds_0

added theorem Real.tendsto_exp_neg_atTop_nhds_zero

deleted theorem Real.tendsto_exp_nhds_0_nhds_1

added theorem Real.tendsto_exp_nhds_zero_nhds_one

deleted theorem Real.tendsto_pow_mul_exp_neg_atTop_nhds_0

added theorem Real.tendsto_pow_mul_exp_neg_atTop_nhds_zero

Modified Mathlib/Analysis/SpecialFunctions/Gamma/Basic.lean

Modified Mathlib/Analysis/SpecialFunctions/Log/Deriv.lean

deleted theorem Real.hasSum_log_sub_log_of_abs_lt_1

added theorem Real.hasSum_log_sub_log_of_abs_lt_one

deleted theorem Real.hasSum_pow_div_log_of_abs_lt_1

added theorem Real.hasSum_pow_div_log_of_abs_lt_one

Modified Mathlib/Analysis/SpecialFunctions/PolynomialExp.lean

Modified Mathlib/Analysis/SpecialFunctions/Pow/Asymptotics.lean

deleted theorem tendsto_rpow_mul_exp_neg_mul_atTop_nhds_0

added theorem tendsto_rpow_mul_exp_neg_mul_atTop_nhds_zero

Modified Mathlib/Analysis/SpecialFunctions/Stirling.lean

Modified Mathlib/Analysis/SpecificLimits/Basic.lean

deleted theorem ENNReal.tendsto_pow_atTop_nhds_0_of_lt_1

added theorem ENNReal.tendsto_pow_atTop_nhds_zero_of_lt_one

deleted theorem NNReal.tendsto_algebraMap_inverse_atTop_nhds_0_nat

added theorem NNReal.tendsto_algebraMap_inverse_atTop_nhds_zero_nat

deleted theorem NNReal.tendsto_const_div_atTop_nhds_0_nat

added theorem NNReal.tendsto_const_div_atTop_nhds_zero_nat

deleted theorem NNReal.tendsto_inverse_atTop_nhds_0_nat

added theorem NNReal.tendsto_inverse_atTop_nhds_zero_nat

deleted theorem NNReal.tendsto_pow_atTop_nhds_0_of_lt_1

added theorem NNReal.tendsto_pow_atTop_nhds_zero_of_lt_one

deleted theorem hasSum_geometric_of_lt_1

added theorem hasSum_geometric_of_lt_one

deleted theorem summable_geometric_of_lt_1

added theorem summable_geometric_of_lt_one

deleted theorem tendsto_algebraMap_inverse_atTop_nhds_0_nat

added theorem tendsto_algebraMap_inverse_atTop_nhds_zero_nat

deleted theorem tendsto_const_div_atTop_nhds_0_nat

added theorem tendsto_const_div_atTop_nhds_zero_nat

deleted theorem tendsto_inverse_atTop_nhds_0_nat

added theorem tendsto_inverse_atTop_nhds_zero_nat

deleted theorem tendsto_one_div_add_atTop_nhds_0_nat

added theorem tendsto_one_div_add_atTop_nhds_zero_nat

deleted theorem tendsto_one_div_atTop_nhds_0_nat

added theorem tendsto_one_div_atTop_nhds_zero_nat

deleted theorem tendsto_pow_atTop_nhdsWithin_0_of_lt_1

added theorem tendsto_pow_atTop_nhdsWithin_zero_of_lt_one

deleted theorem tendsto_pow_atTop_nhds_0_iff

deleted theorem tendsto_pow_atTop_nhds_0_of_lt_1

added theorem tendsto_pow_atTop_nhds_zero_iff

added theorem tendsto_pow_atTop_nhds_zero_of_lt_one

deleted theorem tsum_geometric_of_lt_1

added theorem tsum_geometric_of_lt_one

deleted theorem uniformity_basis_dist_pow_of_lt_1

added theorem uniformity_basis_dist_pow_of_lt_one

Modified Mathlib/Analysis/SpecificLimits/IsROrC.lean

deleted theorem IsROrC.tendsto_inverse_atTop_nhds_0_nat

added theorem IsROrC.tendsto_inverse_atTop_nhds_zero_nat

Modified Mathlib/Analysis/SpecificLimits/Normed.lean

deleted theorem NormedRing.summable_geometric_of_norm_lt_1

added theorem NormedRing.summable_geometric_of_norm_lt_one

deleted theorem NormedRing.tsum_geometric_of_norm_lt_1

added theorem NormedRing.tsum_geometric_of_norm_lt_one

deleted theorem hasSum_coe_mul_geometric_of_norm_lt_1

added theorem hasSum_coe_mul_geometric_of_norm_lt_one

deleted theorem hasSum_geometric_of_abs_lt_1

added theorem hasSum_geometric_of_abs_lt_one

deleted theorem hasSum_geometric_of_norm_lt_1

added theorem hasSum_geometric_of_norm_lt_one

deleted theorem summable_geometric_iff_norm_lt_1

added theorem summable_geometric_iff_norm_lt_one

deleted theorem summable_geometric_of_abs_lt_1

added theorem summable_geometric_of_abs_lt_one

deleted theorem summable_geometric_of_norm_lt_1

added theorem summable_geometric_of_norm_lt_one

deleted theorem summable_norm_pow_mul_geometric_of_norm_lt_1

added theorem summable_norm_pow_mul_geometric_of_norm_lt_one

deleted theorem summable_pow_mul_geometric_of_norm_lt_1

added theorem summable_pow_mul_geometric_of_norm_lt_one

deleted theorem tendsto_pow_atTop_nhds_0_of_abs_lt_1

deleted theorem tendsto_pow_atTop_nhds_0_of_norm_lt_1

added theorem tendsto_pow_atTop_nhds_zero_of_abs_lt_one

added theorem tendsto_pow_atTop_nhds_zero_of_norm_lt_one

deleted theorem tsum_coe_mul_geometric_of_norm_lt_1

added theorem tsum_coe_mul_geometric_of_norm_lt_one

deleted theorem tsum_geometric_of_abs_lt_1

added theorem tsum_geometric_of_abs_lt_one

deleted theorem tsum_geometric_of_norm_lt_1

added theorem tsum_geometric_of_norm_lt_one

Modified Mathlib/Data/Real/Cardinality.lean

Modified Mathlib/Data/Real/Hyperreal.lean

Modified Mathlib/Dynamics/Circle/RotationNumber/TranslationNumber.lean

Modified Mathlib/MeasureTheory/Covering/Besicovitch.lean

Modified Mathlib/MeasureTheory/Covering/LiminfLimsup.lean

Modified Mathlib/MeasureTheory/Decomposition/UnsignedHahn.lean

Modified Mathlib/MeasureTheory/Integral/CircleIntegral.lean

Modified Mathlib/MeasureTheory/Integral/PeakFunction.lean

Modified Mathlib/MeasureTheory/Measure/HasOuterApproxClosed.lean

Modified Mathlib/MeasureTheory/Measure/Lebesgue/EqHaar.lean

Modified Mathlib/NumberTheory/EulerProduct/Basic.lean

Modified Mathlib/NumberTheory/Liouville/LiouvilleNumber.lean

Modified Mathlib/NumberTheory/ModularForms/JacobiTheta/OneVariable.lean

Modified Mathlib/NumberTheory/Padics/Hensel.lean

Modified Mathlib/Probability/Distributions/Geometric.lean

Modified Mathlib/Topology/Algebra/Module/Cardinality.lean

Modified Mathlib/Topology/MetricSpace/Closeds.lean

Modified Mathlib/Topology/MetricSpace/HausdorffDistance.lean

Modified Mathlib/Topology/MetricSpace/PiNat.lean

Modified Mathlib/Topology/MetricSpace/Polish.lean

Modified Mathlib/Topology/TietzeExtension.lean

Modified docs/undergrad.yaml