Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-11-14 12:00 2fc6f911

View on Github →

refactor(algebra/*): streamlining up to data.nat.cast.basic (#17530)

Estimated changes

Modified src/algebra/euclidean_domain/instances.lean

Modified src/algebra/field/basic.lean

Modified src/algebra/group/with_one.lean

Modified src/algebra/group_power/ring.lean

Created src/algebra/group_with_zero/commute.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 ring.mul_inverse_rev'

added theorem ring.mul_inverse_rev

Created src/algebra/group_with_zero/semiconj.lean

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

Renamed src/algebra/group_with_zero/units.lean to src/algebra/group_with_zero/units/basic.lean

deleted theorem coe_div₀

deleted theorem coe_inv₀

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_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_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 def inv_monoid_with_zero_hom

deleted theorem inv_mul_eq_iff_eq_mul₀

deleted theorem inv_mul_eq_one₀

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 one_div_mul_cancel

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

Created src/algebra/group_with_zero/units/lemmas.lean

added theorem coe_div₀

added theorem coe_inv₀

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_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_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 def inv_monoid_with_zero_hom

added theorem inv_mul_eq_iff_eq_mul₀

added theorem inv_mul_eq_one₀

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 one_div_mul_cancel

added theorem units.smul_mk0

Modified src/algebra/hom/equiv/type_tags.lean

Modified src/algebra/hom/equiv/units/group_with_zero.lean

Modified src/algebra/invertible.lean

Modified src/algebra/ring/prod.lean

Modified src/data/int/cast/lemmas.lean

deleted theorem prod.fst_int_cast

deleted theorem prod.snd_int_cast

Created src/data/int/cast/prod.lean

added theorem prod.fst_int_cast

added theorem prod.snd_int_cast

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

deleted theorem prod.fst_nat_cast

deleted theorem prod.snd_nat_cast

Created src/data/nat/cast/prod.lean

added theorem prod.fst_nat_cast

added theorem prod.snd_nat_cast

Modified src/data/rat/lemmas.lean

Modified src/group_theory/perm/basic.lean

Modified src/group_theory/subsemigroup/operations.lean