mathlib

97c4d4ed - feat(analysis/asymptotics/asymptotics): add `is_O.exists_mem_basis` (#13973)