prod — Mathlib

English

The product of two subalgebras S and S₁ of A and B, respectively, is a subalgebra of A × B.

Русский

Произведение подалгебр S ⊆ A и S₁ ⊆ B является подалгеброй в A × B.

LaTeX

$$def prod : Subalgebra R (A × B) := …$$

Lean4

/-- The product of two subalgebras is a subalgebra. -/
def prod : Subalgebra R (A × B) :=
  { S.toSubsemiring.prod S₁.toSubsemiring with
    carrier := S ×ˢ S₁
    algebraMap_mem' := fun _ => ⟨algebraMap_mem _ _, algebraMap_mem _ _⟩ }

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