Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-06-08 17:34 9fba817f

View on Github →

refactor(algebra/*): move commute below ring in imports (#2973) Fixes #1865 API changes:

  • drop lemmas about unbundled center;
  • add to_additive to semiconj_by and commute;
  • drop inv_comm_of_comm in favor of commute.left_inv, same with inv_comm_of_comm and commute.left_inv';
  • rename monoid_hom.map_commute to commute.map, same with semiconj_by;
  • drop commute.cast_*_* and nat/int/rat.mul_cast_comm, add nat/int/rat.cast_commute and nat.int.rat.commute_cast;
  • add commute.mul_fpow.

Estimated changes

deleted def centralizer
deleted theorem commute.add_left
deleted theorem commute.add_right
deleted theorem commute.cast_int_left
deleted theorem commute.cast_int_right
deleted theorem commute.cast_nat_left
deleted theorem commute.cast_nat_right
deleted theorem commute.div_left
deleted theorem commute.div_right
deleted theorem commute.finv_finv
deleted theorem commute.finv_left
deleted theorem commute.finv_left_iff
deleted theorem commute.finv_right
deleted theorem commute.finv_right_iff
deleted theorem commute.gpow_gpow
deleted theorem commute.gpow_gpow_self
deleted theorem commute.gpow_left
deleted theorem commute.gpow_right
deleted theorem commute.gpow_self
deleted theorem commute.gsmul_gsmul
deleted theorem commute.gsmul_left
deleted theorem commute.gsmul_right
deleted theorem commute.gsmul_self
deleted theorem commute.inv_inv
deleted theorem commute.inv_inv_iff
deleted theorem commute.inv_left
deleted theorem commute.inv_left_iff
deleted theorem commute.inv_right
deleted theorem commute.inv_right_iff
deleted theorem commute.list_prod_left
deleted theorem commute.list_prod_right
deleted theorem commute.mul_left
deleted theorem commute.mul_right
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.nsmul_left
deleted theorem commute.nsmul_nsmul
deleted theorem commute.nsmul_right
deleted theorem commute.nsmul_self
deleted theorem commute.one_left
deleted theorem commute.one_right
deleted theorem commute.pow_left
deleted theorem commute.pow_pow
deleted theorem commute.pow_pow_self
deleted theorem commute.pow_right
deleted theorem commute.pow_self
deleted theorem commute.self_gpow
deleted theorem commute.self_gsmul
deleted theorem commute.self_gsmul_gsmul
deleted theorem commute.self_nsmul
deleted theorem commute.self_nsmul_nsmul
deleted theorem commute.self_pow
deleted theorem commute.sub_left
deleted theorem commute.sub_right
deleted theorem commute.units_coe
deleted theorem commute.units_coe_iff
deleted theorem commute.units_inv_left
deleted theorem commute.units_inv_right
deleted theorem commute.units_of_coe
deleted theorem commute.zero_left
deleted theorem commute.zero_right
deleted def commute
deleted theorem group.centralizer_closure
deleted theorem mem_centralizer
deleted theorem neg_pow
deleted theorem ring.centralizer_closure
deleted theorem inv_comm_of_comm
added theorem commute.inv_inv
added theorem commute.inv_inv_iff
added theorem commute.inv_left
added theorem commute.inv_left_iff
added theorem commute.inv_right
added theorem commute.inv_right_iff
added theorem commute.mul_left
added theorem commute.mul_right
added theorem commute.one_left
added theorem commute.one_right
added theorem commute.units_coe
added theorem commute.units_coe_iff
added theorem commute.units_inv_left
added theorem commute.units_of_coe
added def commute
added theorem semiconj_by.conj_mk
added theorem semiconj_by.inv_right
added theorem semiconj_by.mul_left
added theorem semiconj_by.mul_right
added theorem semiconj_by.one_left
added theorem semiconj_by.one_right
added theorem semiconj_by.units_coe
added def semiconj_by
added theorem units.mk_semiconj_by
added theorem commute.gpow_gpow
added theorem commute.gpow_gpow_self
added theorem commute.gpow_left
added theorem commute.gpow_right
added theorem commute.gpow_self
added theorem commute.gsmul_gsmul
added theorem commute.gsmul_left
added theorem commute.gsmul_right
added theorem commute.gsmul_self
added theorem commute.mul_gpow
added theorem commute.mul_pow
added theorem commute.nsmul_left
added theorem commute.nsmul_nsmul
added theorem commute.nsmul_right
added theorem commute.nsmul_self
added theorem commute.pow_left
added theorem commute.pow_pow
added theorem commute.pow_pow_self
added theorem commute.pow_right
added theorem commute.pow_self
added theorem commute.self_gpow
added theorem commute.self_gsmul
added theorem commute.self_nsmul
added theorem commute.self_pow
modified theorem gpow_one
modified theorem mul_gpow
added theorem neg_pow
modified theorem pow_mul_comm'
added theorem semiconj_by.gpow_right
added theorem semiconj_by.gsmul_left
added theorem semiconj_by.nsmul_left
added theorem semiconj_by.pow_right
added theorem units.conj_pow'
added theorem units.conj_pow
added theorem commute.div_left
added theorem commute.div_right
added theorem commute.inv_inv'
added theorem commute.inv_left'
added theorem commute.inv_left_iff'
added theorem commute.inv_right'
added theorem commute.inv_right_iff'
deleted theorem inv_comm_of_comm'
added theorem semiconj_by.div_right
added theorem semiconj_by.inv_right'
added theorem commute.fpow_fpow
added theorem commute.fpow_fpow_self
added theorem commute.fpow_left
added theorem commute.fpow_right
added theorem commute.fpow_self
added theorem commute.mul_fpow
added theorem commute.self_fpow
deleted theorem fpow_mul_comm
modified theorem mul_fpow
added theorem semiconj_by.fpow_right
added theorem commute.add_left
added theorem commute.add_right
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 commute.zero_left
added theorem commute.zero_right
added theorem semiconj_by.add_left
added theorem semiconj_by.add_right
added theorem semiconj_by.neg_left
added theorem semiconj_by.neg_right
added theorem semiconj_by.sub_left
added theorem semiconj_by.sub_right
added theorem semiconj_by.zero_left
added theorem semiconj_by.zero_right
deleted theorem semiconj_by.add_left
deleted theorem semiconj_by.add_right
deleted theorem semiconj_by.cast_nat_left
deleted theorem semiconj_by.conj_mk
deleted theorem semiconj_by.gpow_right
deleted theorem semiconj_by.gsmul_gsmul
deleted theorem semiconj_by.gsmul_left
deleted theorem semiconj_by.gsmul_right
deleted theorem semiconj_by.inv_inv_symm
deleted theorem semiconj_by.inv_right
deleted theorem semiconj_by.inv_right_iff
deleted theorem semiconj_by.inv_symm_left
deleted theorem semiconj_by.mul_left
deleted theorem semiconj_by.mul_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.nsmul_left
deleted theorem semiconj_by.nsmul_nsmul
deleted theorem semiconj_by.nsmul_right
deleted theorem semiconj_by.one_left
deleted theorem semiconj_by.one_right
deleted theorem semiconj_by.pow_right
deleted theorem semiconj_by.sub_left
deleted theorem semiconj_by.sub_right
deleted theorem semiconj_by.units_coe
deleted theorem semiconj_by.units_coe_iff
deleted theorem semiconj_by.units_of_coe
deleted theorem semiconj_by.zero_left
deleted theorem semiconj_by.zero_right
deleted def semiconj_by
deleted theorem units.conj_pow'
deleted theorem units.conj_pow
deleted theorem units.mk_semiconj_by
added theorem int.cast_commute
added theorem int.commute_cast
deleted theorem int.mul_cast_comm
added theorem nat.cast_commute
modified theorem nat.coe_cast_ring_hom
added theorem nat.commute_cast
deleted theorem nat.mul_cast_comm
added theorem rat.cast_commute
added theorem rat.commute_cast
deleted theorem rat.mul_cast_comm