mathlib3
d4884c0d - feat(analysis/asymptotics): use weaker TC assumptions (#14080)

Commit
3 years ago
feat(analysis/asymptotics): use weaker TC assumptions (#14080) Merge `is_o.trans` with `is_o.trans'`: both lemmas previously took one `semi_normed_group` argument on the primed type (corresponding to the primed function), but now only assume `has_norm` on all three types.
Author
Parents
Loading