Commit 2021-05-18 10:47 e6c787fe

feat(algebra/opposites): add has_scalar (opposite α) α instances (#7630) The action is defined as:

lemma op_smul_eq_mul [monoid α] {a a' : α} : op a • a' = a' * a := rfl

We have a few of places in the library where we prove things about r • b, and then extract a proof of a * b = a • b for free. However, we have no way to do this for b * a right now unless multiplication is commutative. By adding this action, we have b * a = op a • b so in many cases could reuse the smul lemma. This instance does not create a diamond:

-- the two paths to `mul_action (opposite α) (opposite α)` are defeq
example [monoid α] : monoid.to_mul_action (opposite α) = opposite.mul_action α (opposite α) := rfl

Zulip