mathlib
1b7e918c - chore(algebra/geom_sum): rename to odd.geom_sum_pos (#14264)

Commit

3 years ago

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

Author

ericrbg

Parents