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.

Estimated changes