formPerm_subsingleton — Mathlib

English

If s is subsingleton, formPerm s h = 1.

Русский

Если s — подвыпуск, то formPerm s h = 1.

LaTeX

$$$\\text{formPerm\_subsingleton}(s,h) = 1$$$

Lean4

theorem formPerm_subsingleton (s : Cycle α) (h : Subsingleton s) : formPerm s h.nodup = 1 :=
  by
  obtain ⟨s⟩ := s
  simp only [formPerm_coe, mk_eq_coe]
  simp only [length_subsingleton_iff, length_coe, mk_eq_coe] at h
  obtain - | ⟨hd, tl⟩ := s
  · simp
  · simp only [length_eq_zero_iff, add_le_iff_nonpos_left, List.length, nonpos_iff_eq_zero] at h
    simp [h]

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