English
The product of two subsemigroups S ⊆ M and T ⊆ N is a subsemigroup of M × N whose carrier is S × T and whose multiplication is componentwise.
Русский
Произведение подполугрупп S ⊆ M и T ⊆ N образует подполугруппу S × T в M × N с популятором S × T и покомпонентным умножением.
LaTeX
$$$S \\subseteq M,\\ T \\subseteq N \\Rightarrow (S\\times T) \\text{ is a subsemigroup of } M\\times N,\\ (a,b)(a',b')=(aa',bb')$$$
Lean4
/-- Given `Subsemigroup`s `s`, `t` of semigroups `M`, `N` respectively, `s × t` as a subsemigroup
of `M × N`. -/
@[to_additive prod /-- Given `AddSubsemigroup`s `s`, `t` of `AddSemigroup`s `A`, `B` respectively,
`s × t` as an `AddSubsemigroup` of `A × B`. -/
]
def prod (s : Subsemigroup M) (t : Subsemigroup N) : Subsemigroup (M × N)
where
carrier := s ×ˢ t
mul_mem' hp hq := ⟨s.mul_mem hp.1 hq.1, t.mul_mem hp.2 hq.2⟩
