card_support_conj — Mathlib

English

The cardinality of the support of a conjugated permutation equals the cardinality of the original permutation’s support.

Русский

Кардинальность опоры коньюгированной перестановки равна кардинальности опоры исходной перестановки.

LaTeX

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

Lean4

theorem card_support_conj : #(σ * τ * σ⁻¹).support = #τ.support := by simp

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