English
Let R and S be nonunital nonassociative rings. Then the direct product R × S, with componentwise addition and multiplication, is again a nonunital nonassociative ring.
Русский
Пусть R и S — кольца без единицы и без ассоциативности. Тогда прямое произведение R × S с операциями сложения и умножения по компонентам образует кольцо без единицы и без ассоциативности.
LaTeX
$$$[ \\text{NonUnitalNonAssocRing }R] \\; [\\text{NonUnitalNonAssocRing }S] \\; \\Rightarrow\\; \\text{NonUnitalNonAssocRing }(R \\times S). $$$
Lean4
instance instNonUnitalNonAssocRing [NonUnitalNonAssocRing R] [NonUnitalNonAssocRing S] :
NonUnitalNonAssocRing (R × S) :=
{ inferInstanceAs (AddCommGroup (R × S)), inferInstanceAs (NonUnitalNonAssocSemiring (R × S)) with }
