Commit 2022-11-28 02:06 dd60a645

View on Github →

feat(Algebra/Ring/Commute): port file (#759) mathlib3 SHA: 76171581280d5b5d1e2d1f4f37e5420357bdc636

  • depends on: #750 porting notes: basically perfect by mathport!
  1. I marked things involving bit0 and bit1 as deprecated, but left them in.
  2. For some reason Commute.add_right and Commute.add_left were marked as dubious translations, and this seemed to be because from Lean 3 we have Distrib, but Lean 4 expected Semiring, so I just #aligned with an ₓ

Estimated changes

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.isUnit_mul_iff
added theorem Commute.units_inv_left
added theorem Commute.units_of_val
added theorem Commute.units_val
added theorem Commute.units_val_iff
added def Units.leftOfMul
added def Units.rightOfMul
added theorem inv_mul_cancel_comm
added theorem isUnit_mul_self_iff
added theorem mul_inv_cancel_comm
deleted theorem SemiconjBy.units_coe
deleted theorem SemiconjBy.units_coe_iff
deleted theorem SemiconjBy.units_of_coe
added theorem SemiconjBy.units_val
deleted theorem succ_nsmul'
deleted theorem Commute.add_left
deleted theorem Commute.add_right
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.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 Units.inv_eq_self_iff
added theorem mul_self_eq_one_iff
added theorem mul_self_sub_mul_self
added theorem mul_self_sub_one