covariant_swap_mul_of_covariant_mul

English

In a commutative semigroup, if multiplication is covariant with respect to a relation, then the swapped multiplication is covariant as well.

Русский

В коммутативной полугруппе если обычная умножение ковариантна, то и перестановка (смешивание аргументов) ковариантна.

LaTeX

$$$\operatorname{Covariant}(\text{swap}(\cdot, \cdot))$ under $\text{Covariant}(\cdot, \cdot)$ and commutativity.$$

Lean4

@[to_additive]
instance covariant_swap_mul_of_covariant_mul [CommSemigroup N] [CovariantClass N N (· * ·) r] :
    CovariantClass N N (swap (· * ·)) r where elim := (covariant_flip_iff N r (· * ·)).mpr CovariantClass.elim

Похожие утверждения