Commit 2026-02-24 22:57 a6992321
View on Github →feat(Analysis/Normed/Module/FiniteDimension): add lemmas on IsTheta and summability (#34914) IsTheta.summable_iff is a natural generalization of IsEquivalent.summable_iff. Some adjacent lemmas now become direct consequences.