prodEquiv — Mathlib

English

The product of NonUnitalSubrings s and t is canonically isomorphic to their Cartesian product as rings.

Русский

Произведение подполь без единицы является канонически изоморфным их декартову произведению как кольцам.

LaTeX

$$$s.prod t \cong_{+*} s \times t$$$

Lean4

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

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