two_dvd_card_support — Mathlib

English

If σ^2 = 1, then 2 divides the size of the support of σ.

Русский

Если σ^2 = 1, то 2 делит размер поддержки σ.

LaTeX

$$$$2 \mid |\sigma.\mathrm{support}|.$$$$

Lean4

theorem two_dvd_card_support {σ : Perm α} (hσ : σ ^ 2 = 1) : 2 ∣ #σ.support :=
  (congr_arg (Dvd.dvd 2) σ.sum_cycleType).mp
    (Multiset.dvd_sum fun n hn => by
      rw [_root_.le_antisymm
          (Nat.le_of_dvd zero_lt_two <| (dvd_of_mem_cycleType hn).trans <| orderOf_dvd_of_pow_eq_one hσ)
          (two_le_of_mem_cycleType hn)])

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