coe_prod — Mathlib

English

The underlying nonunital subalgebra structure of the product matches the product of underlying subalgebras.

Русский

Структура подпалгебры произведения сопоставляет произведение подалгебр.

LaTeX

$$$ (S \\prod S_1).toNonUnitalSubalgebra = S.toNonUnitalSubalgebra.prod S_1.toNonUnitalSubalgebra $$$

Lean4

@[simp, norm_cast]
theorem coe_prod : (prod S S₁ : Set (A × B)) = (S : Set A) ×ˢ S₁ :=
  rfl

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