prodEquiv — Mathlib

English

The product of submonoids is isomorphic to their product as monoids via the Equivalence induced by the product of sets.

Русский

Произведение подмонойдов изоморфно их произведению как моноидов через естественное соответствие множеств.

LaTeX

$$$ (s.prod t) \cong^* (s \times t) $$$

Lean4

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

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