English
Given submonoids s ⊆ M and t ⊆ N, their product s.prod t is a submonoid of M × N consisting of all pairs (m,n) with m ∈ s and n ∈ t.
Русский
Пусть s ⊆ M и t ⊆ N — подмножества моноидов. Их произведение s.prod t является подмономом М×N, состоящим из пар (m,n) с m∈s и n∈t.
LaTeX
$$$ s.prod t = \{(m,n) ∈ M×N \mid m ∈ s \land n ∈ t\}. $$$
Lean4
/-- Given submonoids `s`, `t` of monoids `M`, `N` respectively, `s × t` as a submonoid
of `M × N`. -/
@[to_additive prod /-- Given `AddSubmonoid`s `s`, `t` of `AddMonoid`s `A`, `B` respectively, `s × t`
as an `AddSubmonoid` of `A × B`. -/
]
def prod (s : Submonoid M) (t : Submonoid N) : Submonoid (M × N)
where
carrier := s ×ˢ t
one_mem' := ⟨s.one_mem, t.one_mem⟩
mul_mem' hp hq := ⟨s.mul_mem hp.1 hq.1, t.mul_mem hp.2 hq.2⟩
