Commit 2023-11-01 16:07 e15cc5f6

View on Github →

chore(Data/ZMod/IntUnitsPower): rename lemmas (#8087) This reduces a diff in a future PR (#7866).

Estimated changes

added theorem mul_uzpow
deleted theorem mul_z₂pow
added theorem one_uzpow
deleted theorem one_z₂pow
added theorem uzpow_add
added theorem uzpow_def
added theorem uzpow_mul
added theorem uzpow_natCast
added theorem uzpow_neg
added theorem uzpow_ofNat
added theorem uzpow_one
added theorem uzpow_sub
added theorem uzpow_zero
deleted theorem z₂pow_add
deleted theorem z₂pow_def
deleted theorem z₂pow_mul
deleted theorem z₂pow_natCast
deleted theorem z₂pow_neg
deleted theorem z₂pow_ofNat
deleted theorem z₂pow_one
deleted theorem z₂pow_sub
deleted theorem z₂pow_zero