mem_nsmul_of_ne_zero

Mathlib.Algebra.Order.Group.Multiset

URI: https://scilib.ai/kg/mathlib#Multiset.mem_nsmul_of_ne_zero

English

If n ≠ 0, then a ∈ n • s iff a ∈ s.

Русский

Если n ≠ 0, то a ∈ n • s ⇔ a ∈ s.

LaTeX

$$$ n \neq 0 \Rightarrow (a \in n \cdot s \iff a \in s) $$$

Lean4

theorem mem_nsmul_of_ne_zero {a : α} {s : Multiset α} {n : ℕ} (h0 : n ≠ 0) : a ∈ n • s ↔ a ∈ s := by simp [*]

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

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

Разделы

Аффилиация

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