zero_mem_smul_set

Mathlib.Algebra.GroupWithZero.Action.Pointwise.Set

URI: https://scilib.ai/kg/mathlib#Set.zero_mem_smul_set

English

Same as Set Pi Smul but in alternative formulation.

Русский

То же, что Set Pi Smul, но в другой формулировке.

LaTeX

$$Same as above$$

Lean4

theorem zero_mem_smul_set (h : (0 : β) ∈ t) : (0 : β) ∈ a • t :=
  ⟨0, h, smul_zero _⟩

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

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

Разделы

Аффилиация

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