zero_mem_smul_set_iff

Mathlib.Algebra.GroupWithZero.Action.Pointwise.Set

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

← MathLib Explorer

English

If t contains 0 and a acts on t, then 0 is in a · t.

Русский

Если 0 ∈ t, то 0 ∈ a · t.

LaTeX

$$(0 ∈ t) → (0 ∈ a · t)$$

Lean4

theorem zero_mem_smul_set_iff (ha : a ≠ 0) : (0 : β) ∈ a • t ↔ (0 : β) ∈ t :=
  by
  refine ⟨?_, zero_mem_smul_set⟩
  rintro ⟨b, hb, h⟩
  rwa [(eq_zero_or_eq_zero_of_smul_eq_zero h).resolve_left ha] at hb

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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