mathlib

09960ea1 - feat(algebra/group_power/basic): `two_zsmul` (#12094)

feat(algebra/group_power/basic): `two_zsmul` (#12094) Mark `zpow_two` with `@[to_additive two_zsmul]`. I see no apparent reason for this result not to use `to_additive`, and I found I had a use for the additive version.