Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-12-06 22:38 eec4b70c

View on Github →

feat(algebra/geom_sum): criteria for 0 < geom_sum (#10567)

Estimated changes

modified def geom_sum
modified theorem geom_sum_def
added theorem geom_sum_neg_iff
modified theorem geom_sum_one
added theorem geom_sum_pos
added theorem geom_sum_pos_iff
added theorem geom_sum_pos_of_odd
added theorem geom_sum_succ'
added theorem geom_sum_succ
added theorem geom_sum_two
modified theorem geom_sum_zero
modified def geom_sum₂
modified theorem geom_sum₂_def
modified theorem geom_sum₂_one
modified theorem geom_sum₂_with_one
modified theorem geom_sum₂_zero
added theorem neg_one_geom_sum
modified theorem one_geom_sum
modified theorem op_geom_sum
modified theorem op_geom_sum₂
added theorem zero_geom_sum