Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-11-13 23:50 e2ec84ad

View on Github →

refactor(data/int/basic): move material about units to new file (#17508)

Estimated changes

Modified src/algebra/group_power/ring.lean

Modified src/algebra/ring/basic.lean

deleted theorem commute.add_left

deleted theorem commute.add_right

deleted theorem commute.bit0_left

deleted theorem commute.bit0_right

deleted theorem commute.bit1_left

deleted theorem commute.bit1_right

deleted theorem commute.mul_self_eq_mul_self_iff

deleted theorem commute.mul_self_sub_mul_self_eq'

deleted theorem commute.mul_self_sub_mul_self_eq

deleted theorem commute.neg_left

deleted theorem commute.neg_left_iff

deleted theorem commute.neg_one_left

deleted theorem commute.neg_one_right

deleted theorem commute.neg_right

deleted theorem commute.neg_right_iff

deleted theorem commute.sub_left

deleted theorem commute.sub_right

deleted theorem is_unit.neg

deleted theorem is_unit.neg_iff

deleted theorem is_unit.sub_iff

deleted theorem mul_self_eq_mul_self_iff

deleted theorem mul_self_eq_one_iff

deleted theorem mul_self_sub_mul_self

deleted theorem mul_self_sub_one

deleted theorem semiconj_by.add_left

deleted theorem semiconj_by.add_right

deleted theorem semiconj_by.neg_left

deleted theorem semiconj_by.neg_left_iff

deleted theorem semiconj_by.neg_one_left

deleted theorem semiconj_by.neg_one_right

deleted theorem semiconj_by.neg_right

deleted theorem semiconj_by.neg_right_iff

deleted theorem semiconj_by.sub_left

deleted theorem semiconj_by.sub_right

deleted theorem units.add_divp

deleted theorem units.divp_add

deleted theorem units.divp_add_divp

deleted theorem units.divp_add_divp_same

deleted theorem units.divp_sub

deleted theorem units.divp_sub_divp

deleted theorem units.divp_sub_divp_same

deleted theorem units.inv_eq_self_iff

deleted theorem units.neg_divp

deleted theorem units.sub_divp

Created src/algebra/ring/commute.lean

added theorem commute.add_left

added theorem commute.add_right

added theorem commute.bit0_left

added theorem commute.bit0_right

added theorem commute.bit1_left

added theorem commute.bit1_right

added theorem commute.mul_self_eq_mul_self_iff

added theorem commute.mul_self_sub_mul_self_eq'

added theorem commute.mul_self_sub_mul_self_eq

added theorem commute.neg_left

added theorem commute.neg_left_iff

added theorem commute.neg_one_left

added theorem commute.neg_one_right

added theorem commute.neg_right

added theorem commute.neg_right_iff

added theorem commute.sub_left

added theorem commute.sub_right

added theorem mul_self_eq_mul_self_iff

added theorem mul_self_eq_one_iff

added theorem mul_self_sub_mul_self

added theorem mul_self_sub_one

added theorem units.inv_eq_self_iff

Created src/algebra/ring/semiconj.lean

added theorem semiconj_by.add_left

added theorem semiconj_by.add_right

added theorem semiconj_by.neg_left

added theorem semiconj_by.neg_left_iff

added theorem semiconj_by.neg_one_left

added theorem semiconj_by.neg_one_right

added theorem semiconj_by.neg_right

added theorem semiconj_by.neg_right_iff

added theorem semiconj_by.sub_left

added theorem semiconj_by.sub_right

Created src/algebra/ring/units.lean

added theorem is_unit.neg

added theorem is_unit.neg_iff

added theorem is_unit.sub_iff

added theorem units.add_divp

added theorem units.divp_add

added theorem units.divp_add_divp

added theorem units.divp_add_divp_same

added theorem units.divp_sub

added theorem units.divp_sub_divp

added theorem units.divp_sub_divp_same

added theorem units.neg_divp

added theorem units.sub_divp

Modified src/data/fintype/basic.lean

Modified src/data/int/basic.lean

deleted theorem int.eq_one_or_neg_one_of_mul_eq_neg_one'

deleted theorem int.eq_one_or_neg_one_of_mul_eq_neg_one

deleted theorem int.eq_one_or_neg_one_of_mul_eq_one'

deleted theorem int.eq_one_or_neg_one_of_mul_eq_one

deleted theorem int.is_unit_add_is_unit_eq_is_unit_add_is_unit

deleted theorem int.is_unit_eq_one_or

deleted theorem int.is_unit_eq_or_eq_neg

deleted theorem int.is_unit_iff

deleted theorem int.is_unit_iff_nat_abs_eq

deleted theorem int.is_unit_mul_self

deleted theorem int.mul_eq_neg_one_iff_eq_one_or_neg_one

deleted theorem int.mul_eq_one_iff_eq_one_or_neg_one

deleted theorem int.of_nat_is_unit

deleted theorem int.units_eq_one_or

deleted theorem int.units_nat_abs

Modified src/data/int/order/basic.lean

deleted theorem int.is_unit_iff_abs_eq

Created src/data/int/order/units.lean

added theorem int.is_unit_iff_abs_eq

added theorem int.is_unit_sq

added theorem int.neg_one_pow_ne_zero

added theorem int.sq_eq_one_of_sq_le_three

added theorem int.sq_eq_one_of_sq_lt_four

added theorem int.units_coe_mul_self

added theorem int.units_inv_eq_self

added theorem int.units_mul_self

added theorem int.units_pow_eq_pow_mod_two

added theorem int.units_sq

Modified src/data/int/units.lean

added theorem int.eq_one_or_neg_one_of_mul_eq_neg_one'

added theorem int.eq_one_or_neg_one_of_mul_eq_neg_one

added theorem int.eq_one_or_neg_one_of_mul_eq_one'

added theorem int.eq_one_or_neg_one_of_mul_eq_one

added theorem int.is_unit_add_is_unit_eq_is_unit_add_is_unit

added theorem int.is_unit_eq_one_or

added theorem int.is_unit_eq_or_eq_neg

added theorem int.is_unit_iff

added theorem int.is_unit_iff_nat_abs_eq

added theorem int.is_unit_mul_self

deleted theorem int.is_unit_sq

added theorem int.mul_eq_neg_one_iff_eq_one_or_neg_one

added theorem int.mul_eq_one_iff_eq_one_or_neg_one

deleted theorem int.neg_one_pow_ne_zero

added theorem int.of_nat_is_unit

deleted theorem int.sq_eq_one_of_sq_le_three

deleted theorem int.sq_eq_one_of_sq_lt_four

deleted theorem int.units_coe_mul_self

added theorem int.units_eq_one_or

deleted theorem int.units_inv_eq_self

deleted theorem int.units_mul_self

added theorem int.units_nat_abs

deleted theorem int.units_pow_eq_pow_mod_two

deleted theorem int.units_sq

Modified src/data/nat/basic.lean

deleted theorem nat.add_units_eq_zero

deleted theorem nat.units_eq_one

Modified src/data/nat/cast/basic.lean

Created src/data/nat/units.lean

added theorem nat.add_units_eq_zero

added theorem nat.units_eq_one

Modified src/group_theory/order_of_element.lean

Modified src/group_theory/perm/sign.lean

Modified src/group_theory/submonoid/basic.lean

Modified test/units.lean