zero_mul_subset

Mathlib.Algebra.GroupWithZero.Pointwise.Finset

URI: https://scilib.ai/kg/mathlib#Finset.zero_mul_subset

English

The product of a Finset with the zero Finset is a subset of the zero Finset.

Русский

Произведение Finset с нулевым Finset принадлежит нулевому Finset.

LaTeX

$$$s \cdot 0 \subseteq 0.$$$

Lean4

theorem zero_mul_subset (s : Finset α) : 0 * s ⊆ 0 := by simp [subset_iff, mem_mul]

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru