Theorem summable_of_isBigO'

Modification history

2023-08-10 19:52

Mathlib/Analysis/NormedSpace/FiniteDimension.lean

chore: banish `Type _` and `Sort _` (#6499) …

Modified summable_of_isBigO'View on Github →

2023-05-20 01:06

Mathlib/Analysis/NormedSpace/FiniteDimension.lean

feat: port Analysis.NormedSpace.FiniteDimension (#4123)

Added summable_of_isBigO'View on Github →