Commit 2026-08-24 06:52 be7cb662

View on Github →

refactor(Analysis/Asymptotics): split long file Defs.lean (#42997) Split this > 1500 line file into:

a bare-minimum Defs.lean (204 lines)
Basic.lean: congruence & filter operations (the longest chunk, 534 lines)
Arith.lean: interaction with +, -, constants (465)
Ring.lean: interaction with *, / (261)
Prod.lean: cartesian products (171) Also move the definition of IsEquivalent from Defs.lean into AsymptoticEquivalent.lean, since it is much less used in the library than IsBigO and IsLittleO.

Estimated changes

Modified Mathlib.lean

Created Mathlib/Analysis/Asymptotics/Arith.lean

added theorem Asymptotics.IsBigO.add

added theorem Asymptotics.IsBigO.add_add

added theorem Asymptotics.IsBigO.add_iff_left

added theorem Asymptotics.IsBigO.add_iff_right

added theorem Asymptotics.IsBigO.add_isLittleO

added theorem Asymptotics.IsBigO.congr_of_sub

added theorem Asymptotics.IsBigO.eq_zero_imp

added theorem Asymptotics.IsBigO.sub

added theorem Asymptotics.IsBigO.sub_iff_left

added theorem Asymptotics.IsBigO.sub_iff_right

added theorem Asymptotics.IsBigO.sum

added theorem Asymptotics.IsBigO.sum_congr'

added theorem Asymptotics.IsBigO.sum_congr

added theorem Asymptotics.IsBigO.symm

added theorem Asymptotics.IsBigO.triangle

added theorem Asymptotics.IsBigOWith.add

added theorem Asymptotics.IsBigOWith.add_add

added theorem Asymptotics.IsBigOWith.add_isLittleO

added theorem Asymptotics.IsBigOWith.eq_zero_imp

added theorem Asymptotics.IsBigOWith.sub

added theorem Asymptotics.IsBigOWith.sub_isLittleO

added theorem Asymptotics.IsBigOWith.sum

added theorem Asymptotics.IsBigOWith.sum_congr'

added theorem Asymptotics.IsBigOWith.sum_congr

added theorem Asymptotics.IsBigOWith.symm

added theorem Asymptotics.IsBigOWith.triangle

added theorem Asymptotics.IsLittleO.add

added theorem Asymptotics.IsLittleO.add_add

added theorem Asymptotics.IsLittleO.add_iff_left

added theorem Asymptotics.IsLittleO.add_iff_right

added theorem Asymptotics.IsLittleO.add_isBigO

added theorem Asymptotics.IsLittleO.add_isBigOWith

added theorem Asymptotics.IsLittleO.congr_of_sub

added theorem Asymptotics.IsLittleO.sub

added theorem Asymptotics.IsLittleO.sub_iff_left

added theorem Asymptotics.IsLittleO.sub_iff_right

added theorem Asymptotics.IsLittleO.sum

added theorem Asymptotics.IsLittleO.sum_congr'

added theorem Asymptotics.IsLittleO.sum_congr

added theorem Asymptotics.IsLittleO.symm

added theorem Asymptotics.IsLittleO.triangle

added theorem Asymptotics.isBigOWith_abs_abs

added theorem Asymptotics.isBigOWith_abs_left

added theorem Asymptotics.isBigOWith_abs_right

added theorem Asymptotics.isBigOWith_comm

added theorem Asymptotics.isBigOWith_const_const

added theorem Asymptotics.isBigOWith_neg_left

added theorem Asymptotics.isBigOWith_neg_right

added theorem Asymptotics.isBigOWith_zero'

added theorem Asymptotics.isBigOWith_zero

added theorem Asymptotics.isBigOWith_zero_right_iff

added theorem Asymptotics.isBigO_abs_abs

added theorem Asymptotics.isBigO_abs_left

added theorem Asymptotics.isBigO_abs_right

added theorem Asymptotics.isBigO_comm

added theorem Asymptotics.isBigO_const_const

added theorem Asymptotics.isBigO_const_const_iff

added theorem Asymptotics.isBigO_neg_left

added theorem Asymptotics.isBigO_neg_right

added theorem Asymptotics.isBigO_pure

added theorem Asymptotics.isBigO_refl_left

added theorem Asymptotics.isBigO_zero

added theorem Asymptotics.isBigO_zero_right_iff

added theorem Asymptotics.isLittleO_abs_abs

added theorem Asymptotics.isLittleO_abs_left

added theorem Asymptotics.isLittleO_abs_right

added theorem Asymptotics.isLittleO_comm

added theorem Asymptotics.isLittleO_neg_left

added theorem Asymptotics.isLittleO_neg_right

added theorem Asymptotics.isLittleO_refl_left

added theorem Asymptotics.isLittleO_zero

added theorem Asymptotics.isLittleO_zero_right_iff

Modified Mathlib/Analysis/Asymptotics/AsymptoticEquivalent.lean

added def Asymptotics.IsEquivalent

Created Mathlib/Analysis/Asymptotics/Basic.lean

added theorem Asymptotics.IsBigO.comp_neg_int

added theorem Asymptotics.IsBigO.comp_tendsto

added theorem Asymptotics.IsBigO.congr'

added theorem Asymptotics.IsBigO.congr

added theorem Asymptotics.IsBigO.congr_left

added theorem Asymptotics.IsBigO.congr_right

added theorem Asymptotics.IsBigO.exists_mem_basis

added theorem Asymptotics.IsBigO.exists_nonneg

added theorem Asymptotics.IsBigO.exists_pos

added theorem Asymptotics.IsBigO.isBigOWith

added theorem Asymptotics.IsBigO.mono

added theorem Asymptotics.IsBigO.not_isLittleO

added theorem Asymptotics.IsBigO.sup

added theorem Asymptotics.IsBigO.trans

added theorem Asymptotics.IsBigO.trans_eventuallyEq

added theorem Asymptotics.IsBigO.trans_isLittleO

added theorem Asymptotics.IsBigO.trans_le

added theorem Asymptotics.IsBigOWith.comp_tendsto

added theorem Asymptotics.IsBigOWith.congr'

added theorem Asymptotics.IsBigOWith.congr

added theorem Asymptotics.IsBigOWith.congr_const

added theorem Asymptotics.IsBigOWith.congr_left

added theorem Asymptotics.IsBigOWith.congr_right

added theorem Asymptotics.IsBigOWith.exists_nonneg

added theorem Asymptotics.IsBigOWith.exists_pos

added theorem Asymptotics.IsBigOWith.isBigO

added theorem Asymptotics.IsBigOWith.mono

added theorem Asymptotics.IsBigOWith.sup'

added theorem Asymptotics.IsBigOWith.sup

added theorem Asymptotics.IsBigOWith.trans

added theorem Asymptotics.IsBigOWith.trans_isLittleO

added theorem Asymptotics.IsBigOWith.trans_le

added theorem Asymptotics.IsBigOWith.weaken

added theorem Asymptotics.IsLittleO.comp_tendsto

added theorem Asymptotics.IsLittleO.congr'

added theorem Asymptotics.IsLittleO.congr

added theorem Asymptotics.IsLittleO.congr_left

added theorem Asymptotics.IsLittleO.congr_right

added theorem Asymptotics.IsLittleO.isBigO

added theorem Asymptotics.IsLittleO.isBigOWith

added theorem Asymptotics.IsLittleO.mono

added theorem Asymptotics.IsLittleO.not_isBigO

added theorem Asymptotics.IsLittleO.sup

added theorem Asymptotics.IsLittleO.trans

added theorem Asymptotics.IsLittleO.trans_eventuallyEq

added theorem Asymptotics.IsLittleO.trans_isBigO

added theorem Asymptotics.IsLittleO.trans_isBigOWith

added theorem Asymptotics.IsLittleO.trans_le

added theorem Asymptotics.isBigOWith_bot

added theorem Asymptotics.isBigOWith_congr

added theorem Asymptotics.isBigOWith_insert

added theorem Asymptotics.isBigOWith_inv

added theorem Asymptotics.isBigOWith_map

added theorem Asymptotics.isBigOWith_norm_left

added theorem Asymptotics.isBigOWith_norm_norm

added theorem Asymptotics.isBigOWith_norm_right

added theorem Asymptotics.isBigOWith_of_le'

added theorem Asymptotics.isBigOWith_of_le

added theorem Asymptotics.isBigOWith_pure

added theorem Asymptotics.isBigOWith_refl

added theorem Asymptotics.isBigO_bot

added theorem Asymptotics.isBigO_congr

added theorem Asymptotics.isBigO_iff_eventually

added theorem Asymptotics.isBigO_iff_eventually_isBigOWith

added theorem Asymptotics.isBigO_map

added theorem Asymptotics.isBigO_norm_left

added theorem Asymptotics.isBigO_norm_norm

added theorem Asymptotics.isBigO_norm_right

added theorem Asymptotics.isBigO_of_le'

added theorem Asymptotics.isBigO_of_le

added theorem Asymptotics.isBigO_of_subsingleton

added theorem Asymptotics.isBigO_refl

added theorem Asymptotics.isBigO_sup

added theorem Asymptotics.isLittleO_bot

added theorem Asymptotics.isLittleO_congr

added theorem Asymptotics.isLittleO_iff_nat_mul_le'

added theorem Asymptotics.isLittleO_iff_nat_mul_le

added theorem Asymptotics.isLittleO_iff_nat_mul_le_aux

added theorem Asymptotics.isLittleO_insert

added theorem Asymptotics.isLittleO_irrefl'

added theorem Asymptotics.isLittleO_irrefl

added theorem Asymptotics.isLittleO_map

added theorem Asymptotics.isLittleO_norm_left

added theorem Asymptotics.isLittleO_norm_norm

added theorem Asymptotics.isLittleO_norm_right

added theorem Asymptotics.isLittleO_of_subsingleton

added theorem Asymptotics.isLittleO_sup

added theorem Filter.Eventually.isBigO

added theorem Filter.Eventually.trans_isBigO

added theorem Filter.EventuallyEq.isBigO

added theorem Filter.EventuallyEq.trans_isBigO

added theorem Filter.EventuallyEq.trans_isLittleO

Modified Mathlib/Analysis/Asymptotics/Defs.lean

deleted theorem Asymptotics.IsBigO.add

deleted theorem Asymptotics.IsBigO.add_add

deleted theorem Asymptotics.IsBigO.add_iff_left

deleted theorem Asymptotics.IsBigO.add_iff_right

deleted theorem Asymptotics.IsBigO.add_isLittleO

deleted theorem Asymptotics.IsBigO.comp_neg_int

deleted theorem Asymptotics.IsBigO.comp_tendsto

deleted theorem Asymptotics.IsBigO.congr'

deleted theorem Asymptotics.IsBigO.congr

deleted theorem Asymptotics.IsBigO.congr_left

deleted theorem Asymptotics.IsBigO.congr_of_sub

deleted theorem Asymptotics.IsBigO.congr_right

deleted theorem Asymptotics.IsBigO.const_mul_left

deleted theorem Asymptotics.IsBigO.const_mul_right'

deleted theorem Asymptotics.IsBigO.const_mul_right

deleted theorem Asymptotics.IsBigO.eq_zero_imp

deleted theorem Asymptotics.IsBigO.eventually_mul_div_cancel

deleted theorem Asymptotics.IsBigO.exists_mem_basis

deleted theorem Asymptotics.IsBigO.exists_nonneg

deleted theorem Asymptotics.IsBigO.exists_pos

deleted theorem Asymptotics.IsBigO.inv_rev

deleted theorem Asymptotics.IsBigO.isBigOWith

deleted theorem Asymptotics.IsBigO.mono

deleted theorem Asymptotics.IsBigO.mul

deleted theorem Asymptotics.IsBigO.mul_isLittleO

deleted theorem Asymptotics.IsBigO.not_isLittleO

deleted theorem Asymptotics.IsBigO.of_const_mul_right

deleted theorem Asymptotics.IsBigO.pow

deleted theorem Asymptotics.IsBigO.prod_left

deleted theorem Asymptotics.IsBigO.prod_left_fst

deleted theorem Asymptotics.IsBigO.prod_left_snd

deleted theorem Asymptotics.IsBigO.prod_rightl

deleted theorem Asymptotics.IsBigO.prod_rightr

deleted theorem Asymptotics.IsBigO.sub

deleted theorem Asymptotics.IsBigO.sub_iff_left

deleted theorem Asymptotics.IsBigO.sub_iff_right

deleted theorem Asymptotics.IsBigO.sum

deleted theorem Asymptotics.IsBigO.sum_congr'

deleted theorem Asymptotics.IsBigO.sum_congr

deleted theorem Asymptotics.IsBigO.sup

deleted theorem Asymptotics.IsBigO.symm

deleted theorem Asymptotics.IsBigO.trans

deleted theorem Asymptotics.IsBigO.trans_eventuallyEq

deleted theorem Asymptotics.IsBigO.trans_isLittleO

deleted theorem Asymptotics.IsBigO.trans_le

deleted theorem Asymptotics.IsBigO.triangle

deleted theorem Asymptotics.IsBigOWith.add

deleted theorem Asymptotics.IsBigOWith.add_add

deleted theorem Asymptotics.IsBigOWith.add_isLittleO

deleted theorem Asymptotics.IsBigOWith.comp_tendsto

deleted theorem Asymptotics.IsBigOWith.congr'

deleted theorem Asymptotics.IsBigOWith.congr

deleted theorem Asymptotics.IsBigOWith.congr_const

deleted theorem Asymptotics.IsBigOWith.congr_left

deleted theorem Asymptotics.IsBigOWith.congr_right

deleted theorem Asymptotics.IsBigOWith.const_mul_left

deleted theorem Asymptotics.IsBigOWith.const_mul_right'

deleted theorem Asymptotics.IsBigOWith.const_mul_right

deleted theorem Asymptotics.IsBigOWith.eq_zero_imp

deleted theorem Asymptotics.IsBigOWith.eventually_mul_div_cancel

deleted theorem Asymptotics.IsBigOWith.exists_nonneg

deleted theorem Asymptotics.IsBigOWith.exists_pos

deleted theorem Asymptotics.IsBigOWith.inv_rev

deleted theorem Asymptotics.IsBigOWith.isBigO

deleted theorem Asymptotics.IsBigOWith.mono

deleted theorem Asymptotics.IsBigOWith.mul

deleted theorem Asymptotics.IsBigOWith.of_const_mul_right

deleted theorem Asymptotics.IsBigOWith.of_pow

deleted theorem Asymptotics.IsBigOWith.pow'

deleted theorem Asymptotics.IsBigOWith.pow

deleted theorem Asymptotics.IsBigOWith.prod_left

deleted theorem Asymptotics.IsBigOWith.prod_left_fst

deleted theorem Asymptotics.IsBigOWith.prod_left_same

deleted theorem Asymptotics.IsBigOWith.prod_left_snd

deleted theorem Asymptotics.IsBigOWith.prod_rightl

deleted theorem Asymptotics.IsBigOWith.prod_rightr

deleted theorem Asymptotics.IsBigOWith.sub

deleted theorem Asymptotics.IsBigOWith.sub_isLittleO

deleted theorem Asymptotics.IsBigOWith.sum

deleted theorem Asymptotics.IsBigOWith.sum_congr'

deleted theorem Asymptotics.IsBigOWith.sum_congr

deleted theorem Asymptotics.IsBigOWith.sup'

deleted theorem Asymptotics.IsBigOWith.sup

deleted theorem Asymptotics.IsBigOWith.symm

deleted theorem Asymptotics.IsBigOWith.trans

deleted theorem Asymptotics.IsBigOWith.trans_isLittleO

deleted theorem Asymptotics.IsBigOWith.trans_le

deleted theorem Asymptotics.IsBigOWith.triangle

deleted theorem Asymptotics.IsBigOWith.weaken

deleted def Asymptotics.IsEquivalent

deleted theorem Asymptotics.IsLittleO.add

deleted theorem Asymptotics.IsLittleO.add_add

deleted theorem Asymptotics.IsLittleO.add_iff_left

deleted theorem Asymptotics.IsLittleO.add_iff_right

deleted theorem Asymptotics.IsLittleO.add_isBigO

deleted theorem Asymptotics.IsLittleO.add_isBigOWith

deleted theorem Asymptotics.IsLittleO.comp_tendsto

deleted theorem Asymptotics.IsLittleO.congr'

deleted theorem Asymptotics.IsLittleO.congr

deleted theorem Asymptotics.IsLittleO.congr_left

deleted theorem Asymptotics.IsLittleO.congr_of_sub

deleted theorem Asymptotics.IsLittleO.congr_right

deleted theorem Asymptotics.IsLittleO.const_mul_left

deleted theorem Asymptotics.IsLittleO.const_mul_right'

deleted theorem Asymptotics.IsLittleO.const_mul_right

deleted theorem Asymptotics.IsLittleO.eventually_mul_div_cancel

deleted theorem Asymptotics.IsLittleO.inv_rev

deleted theorem Asymptotics.IsLittleO.isBigO

deleted theorem Asymptotics.IsLittleO.isBigOWith

deleted theorem Asymptotics.IsLittleO.mono

deleted theorem Asymptotics.IsLittleO.mul

deleted theorem Asymptotics.IsLittleO.mul_isBigO

deleted theorem Asymptotics.IsLittleO.not_isBigO

deleted theorem Asymptotics.IsLittleO.of_const_mul_right

deleted theorem Asymptotics.IsLittleO.of_pow

deleted theorem Asymptotics.IsLittleO.pow

deleted theorem Asymptotics.IsLittleO.prod_left

deleted theorem Asymptotics.IsLittleO.prod_left_fst

deleted theorem Asymptotics.IsLittleO.prod_left_snd

deleted theorem Asymptotics.IsLittleO.prod_rightl

deleted theorem Asymptotics.IsLittleO.prod_rightr

deleted theorem Asymptotics.IsLittleO.sub

deleted theorem Asymptotics.IsLittleO.sub_iff_left

deleted theorem Asymptotics.IsLittleO.sub_iff_right

deleted theorem Asymptotics.IsLittleO.sum

deleted theorem Asymptotics.IsLittleO.sum_congr'

deleted theorem Asymptotics.IsLittleO.sum_congr

deleted theorem Asymptotics.IsLittleO.sup

deleted theorem Asymptotics.IsLittleO.symm

deleted theorem Asymptotics.IsLittleO.trans

deleted theorem Asymptotics.IsLittleO.trans_eventuallyEq

deleted theorem Asymptotics.IsLittleO.trans_isBigO

deleted theorem Asymptotics.IsLittleO.trans_isBigOWith

deleted theorem Asymptotics.IsLittleO.trans_le

deleted theorem Asymptotics.IsLittleO.triangle

deleted theorem Asymptotics.isBigOWith_abs_abs

deleted theorem Asymptotics.isBigOWith_abs_left

deleted theorem Asymptotics.isBigOWith_abs_right

deleted theorem Asymptotics.isBigOWith_bot

deleted theorem Asymptotics.isBigOWith_comm

deleted theorem Asymptotics.isBigOWith_congr

deleted theorem Asymptotics.isBigOWith_const_const

deleted theorem Asymptotics.isBigOWith_const_mul_self

deleted theorem Asymptotics.isBigOWith_fst_prod

deleted theorem Asymptotics.isBigOWith_insert

deleted theorem Asymptotics.isBigOWith_inv

deleted theorem Asymptotics.isBigOWith_map

deleted theorem Asymptotics.isBigOWith_neg_left

deleted theorem Asymptotics.isBigOWith_neg_right

deleted theorem Asymptotics.isBigOWith_norm_left

deleted theorem Asymptotics.isBigOWith_norm_norm

deleted theorem Asymptotics.isBigOWith_norm_right

deleted theorem Asymptotics.isBigOWith_of_le'

deleted theorem Asymptotics.isBigOWith_of_le

deleted theorem Asymptotics.isBigOWith_prod_left

deleted theorem Asymptotics.isBigOWith_pure

deleted theorem Asymptotics.isBigOWith_refl

deleted theorem Asymptotics.isBigOWith_self_const_mul'

deleted theorem Asymptotics.isBigOWith_self_const_mul

deleted theorem Asymptotics.isBigOWith_snd_prod

deleted theorem Asymptotics.isBigOWith_zero'

deleted theorem Asymptotics.isBigOWith_zero

deleted theorem Asymptotics.isBigOWith_zero_right_iff

deleted theorem Asymptotics.isBigO_abs_abs

deleted theorem Asymptotics.isBigO_abs_left

deleted theorem Asymptotics.isBigO_abs_right

deleted theorem Asymptotics.isBigO_bot

deleted theorem Asymptotics.isBigO_comm

deleted theorem Asymptotics.isBigO_congr

deleted theorem Asymptotics.isBigO_const_const

deleted theorem Asymptotics.isBigO_const_const_iff

deleted theorem Asymptotics.isBigO_const_mul_left_iff'

deleted theorem Asymptotics.isBigO_const_mul_left_iff

deleted theorem Asymptotics.isBigO_const_mul_right_iff'

deleted theorem Asymptotics.isBigO_const_mul_right_iff

deleted theorem Asymptotics.isBigO_const_mul_self

deleted theorem Asymptotics.isBigO_fst_prod'

deleted theorem Asymptotics.isBigO_fst_prod

modified theorem Asymptotics.isBigO_iff''

modified theorem Asymptotics.isBigO_iff'

deleted theorem Asymptotics.isBigO_iff_eventually

deleted theorem Asymptotics.isBigO_iff_eventually_isBigOWith

deleted theorem Asymptotics.isBigO_map

deleted theorem Asymptotics.isBigO_neg_left

deleted theorem Asymptotics.isBigO_neg_right

deleted theorem Asymptotics.isBigO_norm_left

deleted theorem Asymptotics.isBigO_norm_norm

deleted theorem Asymptotics.isBigO_norm_right

deleted theorem Asymptotics.isBigO_of_le'

deleted theorem Asymptotics.isBigO_of_le

deleted theorem Asymptotics.isBigO_of_subsingleton

deleted theorem Asymptotics.isBigO_prod_left

deleted theorem Asymptotics.isBigO_pure

deleted theorem Asymptotics.isBigO_refl

deleted theorem Asymptotics.isBigO_refl_left

deleted theorem Asymptotics.isBigO_self_const_mul'

deleted theorem Asymptotics.isBigO_self_const_mul

deleted theorem Asymptotics.isBigO_snd_prod'

deleted theorem Asymptotics.isBigO_snd_prod

deleted theorem Asymptotics.isBigO_sup

deleted theorem Asymptotics.isBigO_zero

deleted theorem Asymptotics.isBigO_zero_right_iff

deleted theorem Asymptotics.isLittleO_abs_abs

deleted theorem Asymptotics.isLittleO_abs_left

deleted theorem Asymptotics.isLittleO_abs_right

deleted theorem Asymptotics.isLittleO_bot

deleted theorem Asymptotics.isLittleO_comm

deleted theorem Asymptotics.isLittleO_congr

deleted theorem Asymptotics.isLittleO_const_mul_left_iff'

deleted theorem Asymptotics.isLittleO_const_mul_left_iff

deleted theorem Asymptotics.isLittleO_const_mul_right_iff'

deleted theorem Asymptotics.isLittleO_const_mul_right_iff

deleted theorem Asymptotics.isLittleO_iff_nat_mul_le'

deleted theorem Asymptotics.isLittleO_iff_nat_mul_le

deleted theorem Asymptotics.isLittleO_iff_nat_mul_le_aux

deleted theorem Asymptotics.isLittleO_insert

deleted theorem Asymptotics.isLittleO_irrefl'

deleted theorem Asymptotics.isLittleO_irrefl

deleted theorem Asymptotics.isLittleO_map

deleted theorem Asymptotics.isLittleO_neg_left

deleted theorem Asymptotics.isLittleO_neg_right

deleted theorem Asymptotics.isLittleO_norm_left

deleted theorem Asymptotics.isLittleO_norm_norm

deleted theorem Asymptotics.isLittleO_norm_right

deleted theorem Asymptotics.isLittleO_of_subsingleton

deleted theorem Asymptotics.isLittleO_prod_left

deleted theorem Asymptotics.isLittleO_refl_left

deleted theorem Asymptotics.isLittleO_sup

deleted theorem Asymptotics.isLittleO_zero

deleted theorem Asymptotics.isLittleO_zero_right_iff

deleted theorem Filter.Eventually.isBigO

deleted theorem Filter.Eventually.trans_isBigO

deleted theorem Filter.EventuallyEq.isBigO

deleted theorem Filter.EventuallyEq.trans_isBigO

deleted theorem Filter.EventuallyEq.trans_isLittleO

Modified Mathlib/Analysis/Asymptotics/Lemmas.lean

Created Mathlib/Analysis/Asymptotics/Prod.lean

added theorem Asymptotics.IsBigO.prod_left

added theorem Asymptotics.IsBigO.prod_left_fst

added theorem Asymptotics.IsBigO.prod_left_snd

added theorem Asymptotics.IsBigO.prod_rightl

added theorem Asymptotics.IsBigO.prod_rightr

added theorem Asymptotics.IsBigOWith.prod_left

added theorem Asymptotics.IsBigOWith.prod_left_fst

added theorem Asymptotics.IsBigOWith.prod_left_same

added theorem Asymptotics.IsBigOWith.prod_left_snd

added theorem Asymptotics.IsBigOWith.prod_rightl

added theorem Asymptotics.IsBigOWith.prod_rightr

added theorem Asymptotics.IsLittleO.prod_left

added theorem Asymptotics.IsLittleO.prod_left_fst

added theorem Asymptotics.IsLittleO.prod_left_snd

added theorem Asymptotics.IsLittleO.prod_rightl

added theorem Asymptotics.IsLittleO.prod_rightr

added theorem Asymptotics.isBigOWith_fst_prod

added theorem Asymptotics.isBigOWith_prod_left

added theorem Asymptotics.isBigOWith_snd_prod

added theorem Asymptotics.isBigO_fst_prod'

added theorem Asymptotics.isBigO_fst_prod

added theorem Asymptotics.isBigO_prod_left

added theorem Asymptotics.isBigO_snd_prod'

added theorem Asymptotics.isBigO_snd_prod

added theorem Asymptotics.isLittleO_prod_left

Created Mathlib/Analysis/Asymptotics/Ring.lean

added theorem Asymptotics.IsBigO.const_mul_left

added theorem Asymptotics.IsBigO.const_mul_right'

added theorem Asymptotics.IsBigO.const_mul_right

added theorem Asymptotics.IsBigO.eventually_mul_div_cancel

added theorem Asymptotics.IsBigO.inv_rev

added theorem Asymptotics.IsBigO.mul

added theorem Asymptotics.IsBigO.mul_isLittleO

added theorem Asymptotics.IsBigO.of_const_mul_right

added theorem Asymptotics.IsBigO.pow

added theorem Asymptotics.IsBigOWith.const_mul_left

added theorem Asymptotics.IsBigOWith.const_mul_right'

added theorem Asymptotics.IsBigOWith.const_mul_right

added theorem Asymptotics.IsBigOWith.eventually_mul_div_cancel

added theorem Asymptotics.IsBigOWith.inv_rev

added theorem Asymptotics.IsBigOWith.mul

added theorem Asymptotics.IsBigOWith.of_const_mul_right

added theorem Asymptotics.IsBigOWith.of_pow

added theorem Asymptotics.IsBigOWith.pow'

added theorem Asymptotics.IsBigOWith.pow

added theorem Asymptotics.IsLittleO.const_mul_left

added theorem Asymptotics.IsLittleO.const_mul_right'

added theorem Asymptotics.IsLittleO.const_mul_right

added theorem Asymptotics.IsLittleO.eventually_mul_div_cancel

added theorem Asymptotics.IsLittleO.inv_rev

added theorem Asymptotics.IsLittleO.mul

added theorem Asymptotics.IsLittleO.mul_isBigO

added theorem Asymptotics.IsLittleO.of_const_mul_right

added theorem Asymptotics.IsLittleO.of_pow

added theorem Asymptotics.IsLittleO.pow

added theorem Asymptotics.isBigOWith_const_mul_self

added theorem Asymptotics.isBigOWith_self_const_mul'

added theorem Asymptotics.isBigOWith_self_const_mul

added theorem Asymptotics.isBigO_const_mul_left_iff'

added theorem Asymptotics.isBigO_const_mul_left_iff

added theorem Asymptotics.isBigO_const_mul_right_iff'

added theorem Asymptotics.isBigO_const_mul_right_iff

added theorem Asymptotics.isBigO_const_mul_self

added theorem Asymptotics.isBigO_self_const_mul'

added theorem Asymptotics.isBigO_self_const_mul

added theorem Asymptotics.isLittleO_const_mul_left_iff'

added theorem Asymptotics.isLittleO_const_mul_left_iff

added theorem Asymptotics.isLittleO_const_mul_right_iff'

added theorem Asymptotics.isLittleO_const_mul_right_iff

Modified Mathlib/Analysis/Asymptotics/Theta.lean

Modified Mathlib/Analysis/Normed/Operator/Asymptotics.lean

Modified Mathlib/Analysis/Normed/Operator/BoundedLinearMaps.lean

Modified Mathlib/Computability/AkraBazzi/GrowsPolynomially.lean