Commit 2024-01-20 09:50 8b0b0e7f

View on Github →

chore: Move lemmas about Int.natAbs and zpowersHom (#9806) These can be defined earlier for free. Part of #9411

Estimated changes

deleted theorem AddMonoidHom.apply_int
deleted theorem Int.le_self_sq
deleted theorem Int.natAbs_le_self_sq
deleted theorem Int.natAbs_sq
deleted theorem MonoidHom.apply_mint
deleted theorem bit0_mul
deleted theorem bit1_mul
deleted theorem mul_bit0
deleted theorem mul_bit1
deleted theorem pow_eq
deleted def zmultiplesAddHom
deleted theorem zmultiplesAddHom_apply
deleted def zmultiplesHom
deleted theorem zmultiplesHom_apply
deleted theorem zmultiplesHom_symm_apply
deleted def zpowersHom
deleted theorem zpowersHom_apply
deleted theorem zpowersHom_symm_apply
deleted def zpowersMulHom
deleted theorem zpowersMulHom_apply
deleted theorem zpowersMulHom_symm_apply
added theorem AddMonoidHom.apply_int
added theorem MonoidHom.apply_mint
added def zmultiplesAddHom
added theorem zmultiplesAddHom_apply
added def zmultiplesHom
added theorem zmultiplesHom_apply
added def zpowersHom
added theorem zpowersHom_apply
added theorem zpowersHom_symm_apply
added def zpowersMulHom
added theorem zpowersMulHom_apply
added theorem Int.le_self_sq
added theorem Int.natAbs_le_self_sq
added theorem Int.natAbs_sq
added theorem bit0_mul
added theorem bit1_mul
added theorem mul_bit0
added theorem mul_bit1