English
Under the opposite map, the image of a product reverses the factors: (s * t).image op = t.image op * s.image op.
Русский
При образе через противоположное отображение произведение разворачивает множители: (s * t).image op = t.image op * s.image op.
LaTeX
$$Eq (Finset.image MulOpposite.op (instHMul.hMul s t)) (instHMul.hMul (Finset.image MulOpposite.op t) (Finset.image MulOpposite.op s))$$
Lean4
@[to_additive]
theorem image_op_mul (s t : Finset α) : (s * t).image op = t.image op * s.image op :=
image_image₂_antidistrib op_mul