Mathlib Changelog
v3
Changelog
About
Github
Mathlib v3 is deprecated.
Go to Mathlib v4
Commit
2019-02-09 15:38
484d8648
View on Github →
add geometric sum (
#701
)
feat(data/finset): add range_add_one
feat(algebra/big_operators): geometric sum for semiring, ring and division ring
Estimated changes
Modified
src/algebra/big_operators.lean
added
theorem
geom_sum
added
theorem
geom_sum_mul
added
theorem
geom_sum_mul_add
Modified
src/data/finset.lean
added
theorem
finset.range_add_one