toMultiset_eq_nil

Mathlib.Data.List.Cycle

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

English

s.toMultiset = 0 iff s = nil.

Русский

s.toMultiset равно 0 тогда и только тогда, когда s = nil.

LaTeX

$$$\operatorname{toMultiset}(s) = 0 \iff s = \Cycle.nil$$$

Lean4

@[simp]
theorem toMultiset_eq_nil {s : Cycle α} : s.toMultiset = 0 ↔ s = Cycle.nil :=
  Quotient.inductionOn' s (by simp)

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

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

Разделы

Аффилиация

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