WikiLeanRecent changes · Proposals · Flags · Stats · About

Diff — Timeline of mathematics

Revision #1630 → #2662 · back to history

modifiedInfinite series for the logarithm21c824c23fb7
FieldFrom #1630To #2662
mathlib.declReal.hasSum_pow_div_log_of_abs_lt_1Real.hasSum_pow_div_log_of_abs_lt_one
provenanceaiai-moderated