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.