image_op_mul — Mathlib

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

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