Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-06-01 13:00 f359d55b

View on Github →

feat(analysis/asymptotics/asymptotics): generalize is_O.smul etc (#14487) Allow (k₁ : α → 𝕜) (k₂ : α → 𝕜') instead of (k₁ k₂ : α → 𝕜).

Estimated changes

modified theorem asymptotics.is_O.smul
modified theorem asymptotics.is_O.smul_is_o
modified theorem asymptotics.is_O_with.smul
modified theorem asymptotics.is_o.smul
modified theorem asymptotics.is_o.smul_is_O