card_nsmul

Mathlib.Algebra.Order.Group.Multiset

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

English

Cardinality is compatible with n-smul: card(n • s) = n · card s.

Русский

Кардиналитет совместим с n-разовым умножением: card(n • s) = n · card s.

LaTeX

$$$ \operatorname{card}(n \cdot s) = n \cdot \operatorname{card}(s) $$$

Lean4

@[simp]
theorem card_nsmul (s : Multiset α) (n : ℕ) : card (n • s) = n * card s :=
  cardHom.map_nsmul ..

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

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

Разделы

Аффилиация

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