coe_prod — Mathlib

English

The carrier of the product subalgebra equals the product of the carriers: (prod S S₁).carrier = S.carrier × S₁.carrier.

Русский

Носитель произведения подпалгебр равен произведению носителей: carrier( prod S S₁ ) = carrier(S) × carrier(S₁).

LaTeX

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

Lean4

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

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