Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-11-16 01:17 49ae0e37

View on Github →

chore(topology/algebra/order/basic): move field-parts into new file (#17549) File authorship credits go to:

Benjamin Davidson: #4138
Devon Tuma: #7545
Eric Rodriguez: #15022
Oliver Nash: #16762

Estimated changes

Modified src/algebra/continued_fractions/computation/approximation_corollaries.lean

Modified src/topology/algebra/order/basic.lean

deleted theorem eventually_nhds_within_pos_mul_left

deleted theorem filter.tendsto.at_bot_mul

deleted theorem filter.tendsto.at_bot_mul_neg

deleted theorem filter.tendsto.at_top_mul

deleted theorem filter.tendsto.at_top_mul_neg

deleted theorem filter.tendsto.div_at_top

deleted theorem filter.tendsto.inv_tendsto_at_top

deleted theorem filter.tendsto.inv_tendsto_zero

deleted theorem filter.tendsto.mul_at_bot

deleted theorem filter.tendsto.mul_at_top

deleted theorem filter.tendsto.neg_mul_at_bot

deleted theorem filter.tendsto.neg_mul_at_top

deleted theorem mul_tendsto_nhds_one_nhds_one

deleted theorem mul_tendsto_nhds_zero_left

deleted theorem mul_tendsto_nhds_zero_right

deleted theorem nhds_eq_map_mul_left_nhds_one

deleted theorem nhds_eq_map_mul_right_nhds_one

deleted theorem nhds_within_pos_comap_mul_left

deleted theorem tendsto_const_mul_pow_nhds_iff'

deleted theorem tendsto_const_mul_pow_nhds_iff

deleted theorem tendsto_const_mul_zpow_at_top_nhds_iff

deleted theorem tendsto_const_mul_zpow_at_top_zero

deleted theorem tendsto_inv_at_top_zero'

deleted theorem tendsto_inv_at_top_zero

deleted theorem tendsto_inv_zero_at_top

deleted theorem tendsto_pow_neg_at_top

deleted theorem tendsto_zpow_at_top_zero

Created src/topology/algebra/order/field.lean

added theorem eventually_nhds_within_pos_mul_left

added theorem filter.tendsto.at_bot_mul

added theorem filter.tendsto.at_bot_mul_neg

added theorem filter.tendsto.at_top_mul

added theorem filter.tendsto.at_top_mul_neg

added theorem filter.tendsto.div_at_top

added theorem filter.tendsto.inv_tendsto_at_top

added theorem filter.tendsto.inv_tendsto_zero

added theorem filter.tendsto.mul_at_bot

added theorem filter.tendsto.mul_at_top

added theorem filter.tendsto.neg_mul_at_bot

added theorem filter.tendsto.neg_mul_at_top

added theorem mul_tendsto_nhds_one_nhds_one

added theorem mul_tendsto_nhds_zero_left

added theorem mul_tendsto_nhds_zero_right

added theorem nhds_eq_map_mul_left_nhds_one

added theorem nhds_eq_map_mul_right_nhds_one

added theorem nhds_within_pos_comap_mul_left

added theorem tendsto_const_mul_pow_nhds_iff'

added theorem tendsto_const_mul_pow_nhds_iff

added theorem tendsto_const_mul_zpow_at_top_nhds_iff

added theorem tendsto_const_mul_zpow_at_top_zero

added theorem tendsto_inv_at_top_zero'

added theorem tendsto_inv_at_top_zero

added theorem tendsto_inv_zero_at_top

added theorem tendsto_pow_neg_at_top

added theorem tendsto_zpow_at_top_zero

Modified src/topology/algebra/order/liminf_limsup.lean

Modified src/topology/algebra/with_zero_topology.lean

Modified src/topology/fiber_bundle/trivialization.lean

Modified src/topology/instances/real.lean

Modified src/topology/metric_space/lipschitz.lean