Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-05-22 17:01 1b7e918c

View on Github →

chore(algebra/geom_sum): rename to odd.geom_sum_pos (#14264) allowing dot notation :)

Estimated changes

deleted theorem geom_sum_pos_of_odd
added theorem odd.geom_sum_pos