prod_top — Mathlib

English

The product with the top subsemigroup in one factor yields a straightforward isomorphism with the other factor.

Русский

Произведение с верхним подполугруппом в одном факторе тесно связано с другой стороной через изоморфизм.

LaTeX

$$s.prod ⊤ = s.comap (MulHom.fst M N)$$

Lean4

@[to_additive prod_top]
theorem prod_top (s : Subsemigroup M) : s.prod (⊤ : Subsemigroup N) = s.comap (MulHom.fst M N) :=
  ext fun x => by simp [mem_prod, MulHom.coe_fst]

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