prodEquiv — Mathlib

English

The product of subsemigroups is isomorphic to their direct product as semigroups.

Русский

Произведение подполугрупп изоморфно их прямому произведению как полугруппы.

LaTeX

$$s.prod t ≃* s × t$$

Lean4

/-- The product of subsemigroups is isomorphic to their product as semigroups. -/
@[to_additive prodEquiv /--
    The product of additive subsemigroups is isomorphic to their product as additive semigroups -/
    ]
def prodEquiv (s : Subsemigroup M) (t : Subsemigroup N) : s.prod t ≃* s × t :=
  { (Equiv.Set.prod (s : Set M) (t : Set N)) with map_mul' := fun _ _ => rfl }

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