card_toMultiset

Mathlib.Data.List.Cycle

URI: https://scilib.ai/kg/mathlib#Cycle.card_toMultiset

English

The cardinality of the multiset associated to s equals the length of s.

Русский

Кардинал множества, сопоставленного s, равен длине s.

LaTeX

$$$\operatorname{card}(s.\!\!toMultiset) = \operatorname{length}(s)$$$

Lean4

@[simp]
theorem card_toMultiset (s : Cycle α) : Multiset.card s.toMultiset = s.length :=
  Quotient.inductionOn' s (by simp)

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

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

Разделы

Аффилиация

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