coe_prod — Mathlib

English

The carrier of the product subring equals the cartesian product of carriers: (s.prod t : Set (R × S)) = (s : Set R) × (t : Set S).

Русский

Обозначение носителя подкольца-образа равно декартову произведению носителей: (s.prod t : Set (R × S)) = (s : Set R) × (t : Set S).

LaTeX

$$$ (s.prod t : Set (R \times S)) = (s : Set R) \times (t : Set S) $$$

Lean4

@[norm_cast]
theorem coe_prod (s : Subring R) (t : Subring S) : (s.prod t : Set (R × S)) = (s : Set R) ×ˢ (t : Set S) :=
  rfl

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