Commit 2025-03-21 06:09 4ef6d6e3

View on Github →

chore(Topology/Order): use @[to_additive] (#22463)

Estimated changes

Modified Mathlib/Analysis/Asymptotics/AsymptoticEquivalent.lean

Modified Mathlib/Analysis/Complex/PhragmenLindelof.lean

Modified Mathlib/Analysis/Convex/Gauge.lean

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

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

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

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

Modified Mathlib/Analysis/SpecialFunctions/Trigonometric/ComplexDeriv.lean

Modified Mathlib/Analysis/SpecificLimits/Basic.lean

Modified Mathlib/Computability/AkraBazzi/AkraBazzi.lean

Modified Mathlib/Topology/Algebra/Order/Field.lean

deleted theorem Filter.Tendsto.atBot_mul

added theorem Filter.Tendsto.atBot_mul_pos

deleted theorem Filter.Tendsto.atTop_mul

added theorem Filter.Tendsto.atTop_mul_pos

deleted theorem Filter.Tendsto.mul_atBot

deleted theorem Filter.Tendsto.mul_atTop

added theorem Filter.Tendsto.pos_mul_atBot

added theorem Filter.Tendsto.pos_mul_atTop

Modified Mathlib/Topology/Algebra/Order/Group.lean

deleted theorem continuous_abs

added theorem continuous_mabs

added theorem denseRange_zpow_iff_surjective

deleted theorem denseRange_zsmul_iff_surjective

added theorem not_denseRange_zpow

deleted theorem not_denseRange_zsmul

deleted theorem tendsto_abs_nhdsWithin_zero

added theorem tendsto_mabs_nhdsNE_one

added theorem tendsto_one_iff_mabs_tendsto_one

deleted theorem tendsto_zero_iff_abs_tendsto_zero

Modified Mathlib/Topology/Algebra/PontryaginDual.lean

Modified Mathlib/Topology/Order/LeftRightNhds.lean

deleted theorem Filter.Tendsto.add_atBot

deleted theorem Filter.Tendsto.add_atTop

deleted theorem Filter.Tendsto.atBot_add

added theorem Filter.Tendsto.atBot_mul'

deleted theorem Filter.Tendsto.atTop_add

added theorem Filter.Tendsto.atTop_mul'

added theorem Filter.Tendsto.mul_atBot'

added theorem Filter.Tendsto.mul_atTop'

deleted theorem LinearOrderedAddCommGroup.tendsto_nhds

added theorem LinearOrderedCommGroup.tendsto_nhds

deleted theorem eventually_abs_sub_lt

added theorem eventually_mabs_div_lt

added theorem nhds_basis_Icc_one_lt

deleted theorem nhds_basis_Icc_pos

added theorem nhds_basis_Ioo_one_lt

added theorem nhds_basis_Ioo_one_lt_of_one_lt

deleted theorem nhds_basis_Ioo_pos

deleted theorem nhds_basis_Ioo_pos_of_pos

deleted theorem nhds_basis_abs_sub_lt

added theorem nhds_basis_mabs_div_lt

added theorem nhds_basis_one_mabs_lt

deleted theorem nhds_basis_zero_abs_sub_lt

deleted theorem nhds_eq_iInf_abs_sub

added theorem nhds_eq_iInf_mabs_div

deleted theorem orderTopology_of_nhds_abs

added theorem orderTopology_of_nhds_mabs