zero_smul

Mathlib.Algebra.GroupWithZero.Action.Pointwise.Set

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

English

Any nonempty t satisfies 0 · t = 0.

Русский

Любое непустое t удовлетворяет 0 · t = 0.

LaTeX

$$t.Nonempty → (0 ∈ Set · t) = 0$$

Lean4

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

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

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

Разделы

Аффилиация

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