Commit 2025-07-27 02:54 857f7825
View on Github →feat(ZMod): add to_additive_dont_translate (#27521)
This PR adds the tag @[to_additive_dont_translate] to ZMod, so that it is treated the same as ℕ by to_additive. This allows us to use to_additive in 2 more places.