Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-10-09 11:15 d7c8521e

View on Github →

chore(algebra/group_with_zero/basic): split into two files (#16866)

Estimated changes

Modified src/algebra/divisibility.lean

Modified src/algebra/group_with_zero/basic.lean

deleted theorem commute.div_left

deleted theorem commute.div_right

deleted theorem commute.inv_left_iff₀

deleted theorem commute.inv_left₀

deleted theorem commute.inv_right_iff₀

deleted theorem commute.inv_right₀

deleted theorem commute.ring_inverse_ring_inverse

deleted theorem commute.zero_left

deleted theorem commute.zero_right

deleted theorem div_div_cancel'

deleted theorem div_div_div_cancel_right

deleted theorem div_eq_div_iff

deleted theorem div_eq_iff

deleted theorem div_eq_iff_mul_eq

deleted theorem div_eq_of_eq_mul

deleted theorem div_eq_one_iff_eq

deleted theorem div_eq_zero_iff

deleted theorem div_helper

deleted theorem div_left_inj'

deleted theorem div_mul_cancel

deleted theorem div_mul_cancel_of_imp

deleted theorem div_mul_div_cancel

deleted theorem div_mul_left

deleted theorem div_mul_right

deleted theorem div_ne_zero

deleted theorem div_ne_zero_iff

deleted theorem div_self

deleted theorem divp_mk0

deleted theorem eq_div_iff

deleted theorem eq_div_iff_mul_eq

deleted theorem eq_div_of_mul_eq

deleted theorem eq_inv_mul_iff_mul_eq₀

deleted theorem eq_mul_inv_iff_mul_eq₀

deleted theorem eq_on_inv₀

deleted theorem group_with_zero.eq_zero_or_unit

deleted def inv_monoid_with_zero_hom

deleted theorem inv_mul_eq_iff_eq_mul₀

deleted theorem inv_mul_eq_one₀

deleted theorem is_unit.mk0

deleted theorem is_unit.mul_left_eq_zero

deleted theorem is_unit.mul_right_eq_zero

deleted theorem is_unit.ne_zero

deleted theorem is_unit.ring_inverse

deleted theorem is_unit_iff_ne_zero

deleted theorem is_unit_ring_inverse

deleted theorem is_unit_zero_iff

deleted theorem map_div₀

deleted theorem map_eq_zero

deleted theorem map_inv₀

deleted theorem map_ne_zero

deleted theorem monoid_with_zero.coe_inverse

deleted def monoid_with_zero.inverse

deleted theorem monoid_with_zero.inverse_apply

deleted theorem mul_div_cancel'

deleted theorem mul_div_cancel

deleted theorem mul_div_cancel_left

deleted theorem mul_div_cancel_left_of_imp

deleted theorem mul_div_cancel_of_imp'

deleted theorem mul_div_cancel_of_imp

deleted theorem mul_div_mul_left

deleted theorem mul_div_mul_right

deleted theorem mul_eq_mul_of_div_eq_div

deleted theorem mul_eq_one_iff_eq_inv₀

deleted theorem mul_eq_one_iff_inv_eq₀

deleted theorem mul_inv_eq_iff_eq_mul₀

deleted theorem mul_inv_eq_one₀

deleted theorem mul_mul_div

deleted theorem mul_one_div_cancel

deleted theorem not_is_unit_zero

deleted theorem one_div_mul_cancel

deleted theorem ring.inverse_eq_inv'

deleted theorem ring.inverse_eq_inv

deleted theorem ring.inverse_mul_cancel

deleted theorem ring.inverse_mul_cancel_left

deleted theorem ring.inverse_mul_cancel_right

deleted theorem ring.inverse_non_unit

deleted theorem ring.inverse_one

deleted theorem ring.inverse_unit

deleted theorem ring.inverse_zero

deleted theorem ring.mul_inverse_cancel

deleted theorem ring.mul_inverse_cancel_left

deleted theorem ring.mul_inverse_cancel_right

deleted theorem ring.mul_inverse_rev'

deleted theorem ring.mul_inverse_rev

deleted theorem semiconj_by.div_right

deleted theorem semiconj_by.inv_right_iff₀

deleted theorem semiconj_by.inv_right₀

deleted theorem semiconj_by.inv_symm_left_iff₀

deleted theorem semiconj_by.inv_symm_left₀

deleted theorem semiconj_by.zero_left

deleted theorem semiconj_by.zero_right

deleted theorem units.coe_mk0

deleted theorem units.exists0'

deleted theorem units.exists0

deleted theorem units.exists_iff_ne_zero

deleted theorem units.inv_mul'

deleted def units.mk0

deleted theorem units.mk0_coe

deleted theorem units.mk0_inj

deleted theorem units.mk0_mul

deleted theorem units.mk0_one

deleted theorem units.mul_inv'

deleted theorem units.mul_left_eq_zero

deleted theorem units.mul_right_eq_zero

deleted theorem units.ne_zero

deleted theorem units.smul_mk0

Created src/algebra/group_with_zero/units.lean

added theorem commute.div_left

added theorem commute.div_right

added theorem commute.inv_left_iff₀

added theorem commute.inv_left₀

added theorem commute.inv_right_iff₀

added theorem commute.inv_right₀

added theorem commute.ring_inverse_ring_inverse

added theorem commute.zero_left

added theorem commute.zero_right

added theorem div_div_cancel'

added theorem div_div_div_cancel_right

added theorem div_eq_div_iff

added theorem div_eq_iff

added theorem div_eq_iff_mul_eq

added theorem div_eq_of_eq_mul

added theorem div_eq_one_iff_eq

added theorem div_eq_zero_iff

added theorem div_helper

added theorem div_left_inj'

added theorem div_mul_cancel

added theorem div_mul_cancel_of_imp

added theorem div_mul_div_cancel

added theorem div_mul_left

added theorem div_mul_right

added theorem div_ne_zero

added theorem div_ne_zero_iff

added theorem div_self

added theorem divp_mk0

added theorem eq_div_iff

added theorem eq_div_iff_mul_eq

added theorem eq_div_of_mul_eq

added theorem eq_inv_mul_iff_mul_eq₀

added theorem eq_mul_inv_iff_mul_eq₀

added theorem eq_on_inv₀

added theorem group_with_zero.eq_zero_or_unit

added def inv_monoid_with_zero_hom

added theorem inv_mul_eq_iff_eq_mul₀

added theorem inv_mul_eq_one₀

added theorem is_unit.mk0

added theorem is_unit.mul_left_eq_zero

added theorem is_unit.mul_right_eq_zero

added theorem is_unit.ne_zero

added theorem is_unit.ring_inverse

added theorem is_unit_iff_ne_zero

added theorem is_unit_ring_inverse

added theorem is_unit_zero_iff

added theorem map_div₀

added theorem map_eq_zero

added theorem map_inv₀

added theorem map_ne_zero

added theorem monoid_with_zero.coe_inverse

added def monoid_with_zero.inverse

added theorem monoid_with_zero.inverse_apply

added theorem mul_div_cancel'

added theorem mul_div_cancel

added theorem mul_div_cancel_left

added theorem mul_div_cancel_left_of_imp

added theorem mul_div_cancel_of_imp'

added theorem mul_div_cancel_of_imp

added theorem mul_div_mul_left

added theorem mul_div_mul_right

added theorem mul_eq_mul_of_div_eq_div

added theorem mul_eq_one_iff_eq_inv₀

added theorem mul_eq_one_iff_inv_eq₀

added theorem mul_inv_eq_iff_eq_mul₀

added theorem mul_inv_eq_one₀

added theorem mul_mul_div

added theorem mul_one_div_cancel

added theorem not_is_unit_zero

added theorem one_div_mul_cancel

added theorem ring.inverse_eq_inv'

added theorem ring.inverse_eq_inv

added theorem ring.inverse_mul_cancel

added theorem ring.inverse_mul_cancel_left

added theorem ring.inverse_mul_cancel_right

added theorem ring.inverse_non_unit

added theorem ring.inverse_one

added theorem ring.inverse_unit

added theorem ring.inverse_zero

added theorem ring.mul_inverse_cancel

added theorem ring.mul_inverse_cancel_left

added theorem ring.mul_inverse_cancel_right

added theorem ring.mul_inverse_rev'

added theorem ring.mul_inverse_rev

added theorem semiconj_by.div_right

added theorem semiconj_by.inv_right_iff₀

added theorem semiconj_by.inv_right₀

added theorem semiconj_by.inv_symm_left_iff₀

added theorem semiconj_by.inv_symm_left₀

added theorem semiconj_by.zero_left

added theorem semiconj_by.zero_right

added theorem units.coe_mk0

added theorem units.exists0'

added theorem units.exists0

added theorem units.exists_iff_ne_zero

added theorem units.inv_mul'

added def units.mk0

added theorem units.mk0_coe

added theorem units.mk0_inj

added theorem units.mk0_mul

added theorem units.mk0_one

added theorem units.mul_inv'

added theorem units.mul_left_eq_zero

added theorem units.mul_right_eq_zero

added theorem units.ne_zero

added theorem units.smul_mk0

Modified src/algebra/hom/equiv.lean

Modified src/algebra/hom/ring.lean

Modified src/algebra/regular/basic.lean

Modified src/algebra/ring/basic.lean