Commit 2026-09-30 18:48 18dc857e

View on Github →

feat(Algebra/Divisibility/Basic): divisibility in opposite semigroups (#44366) Add to Mathlib.Algebra.Divisibility.Basic:

  • MulOpposite.op_dvd_op_iff (as @[simp], replacing rightDvd_iff_op_dvd_op)
  • MulOpposite.op_rightDvd_op_iff

Estimated changes

added theorem op_dvd_op_iff
added theorem op_rightDvd_op_iff