grade_eq

Mathlib.Data.Finset.Grade

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

English

For every multiset m, grade Nat m equals its cardinality: grade Nat m = card m.

Русский

Для любого мультсета m верно: grade Nat m = card m.

LaTeX

$$$\operatorname{grade}\, \mathbb{N}\, m = |m|$$$

Lean4

@[simp]
theorem grade_eq (m : Multiset α) : grade ℕ m = card m :=
  rfl

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

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

Разделы

Аффилиация

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