one_product_one — Mathlib

English

The pointwise product of the singleton sets {1} and {1} is the singleton {(1,1)}.

Русский

Пусть в произведении по точечному умножению два множества — это единичные множества {1} и {1}; их произведение равно единичному множеству {(1,1)}.

LaTeX

$$$ 1 \times^\mathrm{S} 1 = 1 $$$

Lean4

@[to_additive (attr := simp)]
theorem one_product_one [One β] : (1 ×ˢ 1 : Finset (α × β)) = 1 := by ext; simp [Prod.ext_iff]

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