English
Given nonunital subrings s ⊆ R and t ⊆ S, their product s.prod t is the NonUnitalSubring of R × S consisting of pairs whose first component lies in s and second in t.
Русский
Два подпольных кольца без единицы s ⊆ R и t ⊆ S образуют произведение s.prod t ⊆ R × S, состоящее из пар (r,s) с r ∈ s и s ∈ t.
LaTeX
$$$\text{prod}(s,t) = \{ (r,s) \in R \times S : r \in s \text{ и } s \in t \}$$$
Lean4
/-- Given `NonUnitalSubring`s `s`, `t` of rings `R`, `S` respectively, `s.prod t` is `s ×ˢ t`
as a `NonUnitalSubring` of `R × S`. -/
def prod (s : NonUnitalSubring R) (t : NonUnitalSubring S) : NonUnitalSubring (R × S) :=
{ s.toSubsemigroup.prod t.toSubsemigroup, s.toAddSubgroup.prod t.toAddSubgroup with carrier := s ×ˢ t }
