prod — Mathlib

English

Given nonunital subsemirings s and t, s.prod t is the nonunital subsemiring of R × S with carrier (s × t).

Русский

Пусть даны подполусемиринги s и t; тогда s.prod t — это неупорядоченный подсемиринг в R × S с породкой (s × t).

LaTeX

$$$ (s.prod t : Set(R \\times S)) = (s : Set R) \\times (t : Set S) $$$

Lean4

/-- Given `NonUnitalSubsemiring`s `s`, `t` of semirings `R`, `S` respectively, `s.prod t` is
`s × t` as a non-unital subsemiring of `R × S`. -/
def prod (s : NonUnitalSubsemiring R) (t : NonUnitalSubsemiring S) : NonUnitalSubsemiring (R × S) :=
  { s.toSubsemigroup.prod t.toSubsemigroup, s.toAddSubmonoid.prod t.toAddSubmonoid with
    carrier := (s : Set R) ×ˢ (t : Set S) }

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