support_conj — Mathlib

English

Conjugating a permutation by another preserves the size of its support: #(σ τ σ⁻¹).support = #τ.support.

Русский

Сопряжение перестановки другим сохраняет размер опоры: #(σ τ σ⁻¹).support = #τ.support.

LaTeX

$$$(\sigma * \tau * \sigma^{-1}).\operatorname{support} = \tau.\operatorname{support}$$$

Lean4

@[simp]
theorem support_conj : (σ * τ * σ⁻¹).support = τ.support.map σ.toEmbedding :=
  by
  ext
  simp only [mem_map_equiv, Perm.coe_mul, Function.comp_apply, Ne, Perm.mem_support, Equiv.eq_symm_apply, inv_def]

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