Commit 2022-07-13 02:40 c6014bd2
View on Github →feat(algebra/parity): more general odd.pos (#15186)
The old version of this lemma (added in #13040) was only for ℕ and didn't allow dot notation. We remove this and add a version for canonically_ordered_comm_semirings, and if the definition of odd changes, this will also work for canononically_ordered_add_monoids.