English
The sign of the right-congruence permutation equals the product of the signs of the components.
Русский
Знак правой конгруэнтности равен произведению знаков компонент.
LaTeX
$$$\\operatorname{sign}(\\operatorname{prodCongrRight}(\\sigma)) = \\prod k\\; \\operatorname{sign}(\\sigma(k))$$$
Lean4
theorem sign_prodCongrRight (σ : α → Perm β) : sign (prodCongrRight σ) = ∏ k, sign (σ k) :=
by
obtain ⟨l, hl, mem_l⟩ := Finite.exists_univ_list α
have l_to_finset : l.toFinset = Finset.univ := by
apply eq_top_iff.mpr
intro b _
exact List.mem_toFinset.mpr (mem_l b)
rw [← prod_prodExtendRight σ hl mem_l, map_list_prod sign, List.map_map, ← l_to_finset, List.prod_toFinset _ hl]
simp_rw [← fun a => sign_prodExtendRight a (σ a), Function.comp_def]
