Commit 2023-10-23 14:19 759f2afe

View on Github →

feat(Data/ZMod/IntUnitsPower): The power operator by ZMod 2 on ℤˣ (#7661) Zulip thread

Estimated changes

added theorem Int.units_div_eq_mul
added theorem mul_z₂pow
added theorem one_z₂pow
added theorem z₂pow_add
added theorem z₂pow_def
added theorem z₂pow_mul
added theorem z₂pow_natCast
added theorem z₂pow_neg
added theorem z₂pow_ofNat
added theorem z₂pow_one
added theorem z₂pow_sub
added theorem z₂pow_zero