Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-06-16 02:53 6834a24e

View on Github →

feat(analysis/asymptotics): define is_Theta (#14567)

  • define f =Θ[l] g and prove basic properties;
  • add is_O.const_smul_left, is_o.const_smul_left;
  • rename is_O_const_smul_left_iff and is_o_const_smul_left_iff to is_O_const_smul_left and is_o_const_smul_left.

Estimated changes