zero_smul

Mathlib.Algebra.GroupWithZero.Action.Pointwise.Finset

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

English

Equivalence relating zero smul of a Finset to membership in the Finset after smul.

Русский

Эквив. между нулевым смулом Finset и членством после смула.

LaTeX

$$$ (s : Finset β) : (0 : Finset α) • s = 0$ и эквивалентно чему-то условию.$$

Lean4

theorem zero_smul (ht : t.Nonempty) : (0 : Finset α) • t = 0 :=
  t.zero_smul_subset.antisymm <| by simpa [mem_smul] using ht

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

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

Разделы

Аффилиация

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