sym2_eq_zero_iff

Mathlib.Data.Multiset.Sym

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

English

For any m, m.sym2 = 0 iff m = 0.

Русский

Для любого m: m.sym2 = 0 эквивалентно m = 0.

LaTeX

$$$ m.sym2 = 0 \\iff m = 0 $$$

Lean4

@[simp]
theorem sym2_eq_zero_iff {m : Multiset α} : m.sym2 = 0 ↔ m = 0 :=
  m.inductionOn fun xs => by simp

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

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

Разделы

Аффилиация

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