mul_zero

Mathlib.Algebra.GroupWithZero.Pointwise.Finset

URI: https://scilib.ai/kg/mathlib#Finset.Nonempty.mul_zero

English

For Finset s, under left-cancellation with zero, |s| ≤ |s·s|.

Русский

Для Finset s при левостороннем отменяемом умножении на ноль выполняется |s| ≤ |s·s|.

LaTeX

$$$|s| \le |s \cdot s|.$$$

Lean4

theorem mul_zero (hs : s.Nonempty) : s * 0 = 0 :=
  s.mul_zero_subset.antisymm <| by simpa [mem_mul] using hs

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

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

Разделы

Аффилиация

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