Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-10-24 00:47 08977be6

View on Github →

feat(algebra/semiconj): define semiconj_by and some operations (#1576)

  • feat(algebra/semiconj): define semiconj_by and some operations Also rewrite algebra/commute to reuse results from algebra/semiconj.
  • Some @[simp] attributes
  • Fixes by @rwbarton, more docs
  • Add two more constructors

Estimated changes

modified theorem commute.add_left
modified theorem commute.add_right
modified theorem commute.cast_nat_left
modified theorem commute.cast_nat_right
modified theorem commute.gpow_gpow
modified theorem commute.gpow_gpow_self
modified theorem commute.gpow_left
modified theorem commute.gpow_right
modified theorem commute.gsmul_gsmul
modified theorem commute.gsmul_left
modified theorem commute.gsmul_right
modified theorem commute.gsmul_self
modified theorem commute.inv_inv
modified theorem commute.inv_inv_iff
modified theorem commute.inv_left
modified theorem commute.inv_left_iff
modified theorem commute.inv_right
modified theorem commute.inv_right_iff
modified theorem commute.list_prod_left
modified theorem commute.list_prod_right
modified theorem commute.neg_left
modified theorem commute.neg_left_iff
modified theorem commute.neg_one_left
modified theorem commute.neg_one_right
modified theorem commute.neg_right
modified theorem commute.neg_right_iff
modified theorem commute.one_left
modified theorem commute.one_right
modified theorem commute.pow_pow
modified theorem commute.pow_right
modified theorem commute.self_gsmul
modified theorem commute.self_gsmul_gsmul
modified theorem commute.self_smul
modified theorem commute.self_smul_smul
modified theorem commute.smul_left
modified theorem commute.smul_right
modified theorem commute.smul_self
modified theorem commute.smul_smul
modified theorem commute.sub_left
modified theorem commute.sub_right
modified theorem commute.units_coe
added theorem commute.units_coe_iff
modified theorem commute.units_inv_left
modified theorem commute.units_inv_right
added theorem commute.units_of_coe
modified theorem commute.zero_left
modified theorem commute.zero_right
modified def commute
added theorem semiconj_by.add_left
added theorem semiconj_by.add_right
added theorem semiconj_by.conj_mk
added theorem semiconj_by.gpow_right
added theorem semiconj_by.gsmul_left
added theorem semiconj_by.inv_right
added theorem semiconj_by.mul_left
added theorem semiconj_by.mul_right
added theorem semiconj_by.neg_left
added theorem semiconj_by.neg_right
added theorem semiconj_by.one_left
added theorem semiconj_by.one_right
added theorem semiconj_by.pow_right
added theorem semiconj_by.smul_left
added theorem semiconj_by.smul_right
added theorem semiconj_by.smul_smul
added theorem semiconj_by.sub_left
added theorem semiconj_by.sub_right
added theorem semiconj_by.units_coe
added theorem semiconj_by.zero_left
added theorem semiconj_by.zero_right
added def semiconj_by