Commit 2025-01-07 17:10 db72affa
View on Github →chore: to_additive various results on groups, group actions (#20547) Two adjustments to #20498 that had been requested by Yaël but hadn't been implemented on time before merge.
chore: to_additive various results on groups, group actions (#20547) Two adjustments to #20498 that had been requested by Yaël but hadn't been implemented on time before merge.