Commit 2023-11-04 14:26 0a1d2bb8

refactor(Data/ZMod/IntUnitsPower): generalize ZMod 2 to work for Nat and Int too (#7866) Instead of providing instance : Pow ℤˣ (ZMod 2), this now provides instance [Module R (Additive ℤˣ)] : Pow ℤˣ R. It turns out that this instance already exists for ℕ and ℤ, so all we need to do is create instance : Module (ZMod 2) (Additive ℤˣ) and we obtain new definitions that generalize over all three types. As a result of the generalization, z₂pow has been renamed in lemmas to uzpow (units of ℤ). The motivation here is that I need $(-1) ^ i$ to make sense (and be lawful) for ZMod 2 (on clifford algebras) and ℕ (on exterior algebras). Zulip thread