prodEquiv — Mathlib

English

The product of subsemirings s.prod t is ring-equivalent to the cartesian product s × t via the natural map, i.e., there is a ring isomorphism s.prod t ≃+* s × t.

Русский

Произведение подполумемирингов s.prod t изоморфно через естественный биективный переход к произведению на множества — s × t.

LaTeX

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

Lean4

/-- Product of subsemirings is isomorphic to their product as monoids. -/
def prodEquiv (s : Subsemiring R) (t : Subsemiring S) : s.prod t ≃+* s × t :=
  { Equiv.Set.prod (s : Set R) (t : Set S) with
    map_mul' := fun _ _ => rfl
    map_add' := fun _ _ => rfl }

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