sign_subtypeCongr — Mathlib

English

The sign of the subtype-conjugation of two subtype-permutations equals the product of the signs.

Русский

Знак подтипного сопряжения двух подтиповых перестановок равен произведению знаков.

LaTeX

$$$\\operatorname{sign}(\\operatorname{subtypeCongr}(\\text{ep},\\text{en})) = \\operatorname{sign}(\\text{ep}) \\cdot \\operatorname{sign}(\\text{en})$$$

Lean4

@[simp]
theorem sign_subtypeCongr {p : α → Prop} [DecidablePred p] (ep : Perm { a // p a }) (en : Perm { a // ¬p a }) :
    sign (ep.subtypeCongr en) = sign ep * sign en := by simp [subtypeCongr]

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