mathlib
6834a24e - feat(analysis/asymptotics): define `is_Theta` (#14567)

Commit
3 years ago
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`.
Author
Parents
Loading