coe_card

Mathlib.Data.Multiset.Defs

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

English

The cardinality of the multiset formed from a list equals the length of the list.

Русский

Кардинал мультисета, образованного из списка, равен длине этого списка.

LaTeX

$$$\\operatorname{card}(\\operatorname{ofList}l)=\\operatorname{length}(l).$$$

Lean4

@[simp]
theorem coe_card (l : List α) : card (l : Multiset α) = length l :=
  rfl

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

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

Разделы

Аффилиация

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