map_op_mul — Mathlib

English

The image under a MulHom respects multiplication: (s * t).image f = s.image f * t.image f.

Русский

Образ под умножением через MulHom сохраняется: (s * t).image f = s.image f * t.image f.

LaTeX

$$Eq (Finset.image (instHMul.coe f) (instHMul.hMul s t)) (instHMul.hMul (Finset.image (instHMul.coe f) s) (Finset.image (instHMul.coe f) t))$$

Lean4

@[to_additive]
theorem map_op_mul (s t : Finset α) :
    (s * t).map opEquiv.toEmbedding = t.map opEquiv.toEmbedding * s.map opEquiv.toEmbedding := by
  simp [map_eq_image, image_op_mul]

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