Commit 2025-01-11 00:45 64c71eb1

View on Github →

chore: split Mathlib/Algebra/Group/Int (#20624) Follows the existing split for Mathlib/Algebra/Group/Nat.

Estimated changes

deleted theorem Int.emod_two_ne_one
deleted theorem Int.emod_two_ne_zero
deleted theorem Int.eq_of_mul_eq_one
deleted theorem Int.even_add
deleted theorem Int.even_add_one
deleted theorem Int.even_coe_nat
deleted theorem Int.even_iff
deleted theorem Int.even_mul
deleted theorem Int.even_pow'
deleted theorem Int.even_pow
deleted theorem Int.even_sub
deleted theorem Int.even_sub_one
deleted theorem Int.isUnit_eq_one_or
deleted theorem Int.isUnit_eq_or_eq_neg
deleted theorem Int.isUnit_iff
deleted theorem Int.isUnit_iff_natAbs_eq
deleted theorem Int.isUnit_mul_self
deleted theorem Int.isUnit_ne_iff_eq_neg
deleted theorem Int.natAbs_of_isUnit
deleted theorem Int.not_even_iff
deleted theorem Int.not_even_one
deleted theorem Int.ofAdd_mul
deleted theorem Int.ofNat_isUnit
deleted theorem Int.one_emod_two
deleted theorem Int.toAdd_pow
deleted theorem Int.toAdd_zpow
deleted theorem Int.two_dvd_ne_zero
deleted theorem Int.units_natAbs
deleted theorem zsmul_int_int
deleted theorem zsmul_int_one
added theorem zsmul_int_int
added theorem zsmul_int_one
added theorem Int.emod_two_ne_one
added theorem Int.emod_two_ne_zero
added theorem Int.even_add
added theorem Int.even_add_one
added theorem Int.even_coe_nat
added theorem Int.even_iff
added theorem Int.even_mul
added theorem Int.even_pow'
added theorem Int.even_pow
added theorem Int.even_sub
added theorem Int.even_sub_one
added theorem Int.not_even_iff
added theorem Int.not_even_one
added theorem Int.one_emod_two
added theorem Int.two_dvd_ne_zero
added theorem Int.ofAdd_mul
added theorem Int.toAdd_pow
added theorem Int.toAdd_zpow
added theorem Int.eq_of_mul_eq_one
added theorem Int.isUnit_eq_one_or
added theorem Int.isUnit_iff
added theorem Int.isUnit_mul_self
added theorem Int.natAbs_of_isUnit
added theorem Int.ofNat_isUnit
added theorem Int.units_natAbs