count_nsmul

Mathlib.Algebra.Order.Group.Multiset

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

English

For any a ∈ α, n ∈ ℕ, and s ∈ Multiset α, count a (n • s) = n · count a s.

Русский

Для любого a ∈ α, n ∈ ℕ и s ∈ Multiset α, count a (n • s) = n · count a s.

LaTeX

$$$\operatorname{count} a (n \cdot s) = n \cdot \operatorname{count} a s.$$$

Lean4

@[simp]
theorem count_nsmul (a : α) (n s) : count a (n • s) = n * count a s := by
  induction n <;> simp [*, succ_nsmul, succ_mul, zero_nsmul]

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

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

Разделы

Аффилиация

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