instNonAssocRing — Mathlib

English

If R and S are nonassociative rings, then the product R × S is a nonassociative ring.

Русский

Если R и S — неассоциативные кольца, то их произведение R × S образует неассоциативное кольцо.

LaTeX

$$$[ \\text{NonAssocRing }R] \\; [\\text{NonAssocRing }S] \\; \\Rightarrow\\; \\text{NonAssocRing }(R \\times S). $$$

Lean4

instance instNonAssocRing [NonAssocRing R] [NonAssocRing S] : NonAssocRing (R × S) :=
  { inferInstanceAs (NonUnitalNonAssocRing (R × S)), inferInstanceAs (NonAssocSemiring (R × S)),
    inferInstanceAs (AddGroupWithOne (R × S)) with }

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