Commit 2024-06-04 14:50 925198ab

View on Github →

chore: Delete Data.Int.Parity (#12904) Scatter the lemmas in Data.Int.Parity to earlier files:

Algebra.Group.Int
Algebra.Ring.Int

Estimated changes

Modified Archive/Imo/Imo1998Q2.lean

Modified Mathlib.lean

Modified Mathlib/Algebra/Field/Power.lean

Modified Mathlib/Algebra/Group/Int.lean

added theorem Int.ediv_two_mul_two_of_even

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.two_mul_ediv_two_of_even

added theorem Int.two_not_dvd_two_mul_add_one

Modified Mathlib/Algebra/Order/Field/Power.lean

Modified Mathlib/Algebra/Order/Ring/Int.lean

added theorem Int.isCompl_even_odd

Modified Mathlib/Algebra/Order/Ring/Nat.lean

added theorem Nat.isCompl_even_odd

Modified Mathlib/Algebra/Ring/Int.lean

added theorem Int.Odd.of_mul_left

added theorem Int.Odd.of_mul_right

added theorem Int.add_one_ediv_two_mul_two_of_odd

added theorem Int.ediv_two_mul_two_add_one_of_odd

added theorem Int.even_add'

added theorem Int.even_iff_not_odd

added theorem Int.even_mul_pred_self

added theorem Int.even_mul_succ_self

added theorem Int.even_or_odd'

added theorem Int.even_or_odd

added theorem Int.even_sub'

added theorem Int.even_xor'_odd'

added theorem Int.even_xor'_odd

added theorem Int.four_dvd_add_or_sub_of_odd

added theorem Int.natAbs_even

added theorem Int.natAbs_odd

added theorem Int.ne_of_odd_add

added theorem Int.not_even_bit1

added theorem Int.not_odd_iff

added theorem Int.odd_add'

added theorem Int.odd_add

added theorem Int.odd_coe_nat

added theorem Int.odd_iff

added theorem Int.odd_iff_not_even

added theorem Int.odd_mul

added theorem Int.odd_pow'

added theorem Int.odd_pow

added theorem Int.odd_sub'

added theorem Int.odd_sub

added theorem Int.two_mul_ediv_two_add_one_of_odd

added theorem Int.two_mul_ediv_two_of_odd

Modified Mathlib/Algebra/Ring/NegOnePow.lean

Modified Mathlib/Algebra/Ring/Parity.lean

deleted theorem Nat.isCompl_even_odd

Deleted Mathlib/Data/Int/Parity.lean

deleted theorem Int.Odd.of_mul_left

deleted theorem Int.Odd.of_mul_right

deleted theorem Int.add_one_ediv_two_mul_two_of_odd

deleted theorem Int.ediv_two_mul_two_add_one_of_odd

deleted theorem Int.ediv_two_mul_two_of_even

deleted theorem Int.emod_two_ne_one

deleted theorem Int.emod_two_ne_zero

deleted theorem Int.even_add'

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_iff_not_odd

deleted theorem Int.even_mul

deleted theorem Int.even_mul_pred_self

deleted theorem Int.even_mul_succ_self

deleted theorem Int.even_or_odd'

deleted theorem Int.even_or_odd

deleted theorem Int.even_pow'

deleted theorem Int.even_pow

deleted theorem Int.even_sub'

deleted theorem Int.even_sub

deleted theorem Int.even_sub_one

deleted theorem Int.even_xor'_odd'

deleted theorem Int.even_xor'_odd

deleted theorem Int.four_dvd_add_or_sub_of_odd

deleted theorem Int.isCompl_even_odd

deleted theorem Int.natAbs_even

deleted theorem Int.natAbs_odd

deleted theorem Int.ne_of_odd_add

deleted theorem Int.not_even_bit1

deleted theorem Int.not_even_iff

deleted theorem Int.not_even_one

deleted theorem Int.not_odd_iff

deleted theorem Int.odd_add'

deleted theorem Int.odd_add

deleted theorem Int.odd_coe_nat

deleted theorem Int.odd_iff

deleted theorem Int.odd_iff_not_even

deleted theorem Int.odd_mul

deleted theorem Int.odd_pow'

deleted theorem Int.odd_pow

deleted theorem Int.odd_sub'

deleted theorem Int.odd_sub

deleted theorem Int.one_emod_two

deleted theorem Int.two_dvd_ne_zero

deleted theorem Int.two_mul_ediv_two_add_one_of_odd

deleted theorem Int.two_mul_ediv_two_of_even

deleted theorem Int.two_mul_ediv_two_of_odd

deleted theorem Int.two_not_dvd_two_mul_add_one

Modified Mathlib/GroupTheory/Coxeter/Basic.lean

Modified Mathlib/NumberTheory/Multiplicity.lean

Modified Mathlib/NumberTheory/NumberField/Basic.lean

Modified Mathlib/NumberTheory/SumFourSquares.lean