English
If S ⊆ A and S1 ⊆ B are nonunital subalgebras over a commutative semiring R, then the product S × S1 is a nonunital subalgebra of A × B with carrier S × S1 and closed under scalar action.
Русский
Если S ⊆ A и S1 ⊆ B — ненулевые подпольные подалгебры над коммутативным полем R, то их произведение S × S1 образует ненулевую подпольную подалгебру в A × B, с носителем S × S1 и замкнутостью относительно действия скаляров.
LaTeX
$$$ \\text{prod}(S,S_1) = \\{(a,b) \\mid a \\in S \\text{ и } b \\in S_1\\} \\text{ является } \\text{NonUnitalSubalgebra}_R(A\\times B). $$$
Lean4
/-- The product of two non-unital subalgebras is a non-unital subalgebra. -/
def prod : NonUnitalSubalgebra R (A × B) :=
{
S.toNonUnitalSubsemiring.prod S₁.toNonUnitalSubsemiring with
carrier := S ×ˢ S₁
smul_mem' := fun r _x hx => ⟨SMulMemClass.smul_mem r hx.1, SMulMemClass.smul_mem r hx.2⟩ }
