English
signAux3 assigns to a permutation f and a multiset s a value in ℤˣ, provided with a membership condition that s contains all non-fixed points of f, and is independent of the particular representative of s.
Русский
signAux3 присваивает перестановке f и мультимножеству s значение в ℤˣ, если s содержит все нефиксированные точки f и не зависит от выбора представления s.
LaTeX
$$$\text{signAux3} : \text{Perm}(\alpha) \to \text{Multiset}(\alpha) \to \mathbb{Z}^\times$ с условием: \text{для Finite } \alpha, \text{ при } s: \forall x\, (x\in s) \text{ и } (\text{ NonFixedPoints}(f) \subseteq s) \; \text{получаем} \ldots$$$
Lean4
/-- When the multiset `s : Multiset α` contains all nonfixed points of the permutation `f : Perm α`,
`signAux2 f _` recursively calculates the sign of `f`. -/
def signAux3 [Finite α] (f : Perm α) {s : Multiset α} : (∀ x, x ∈ s) → ℤˣ :=
Quotient.hrecOn s (fun l _ => signAux2 l f) fun l₁ l₂ h ↦
by
rcases Finite.exists_equiv_fin α with ⟨n, ⟨e⟩⟩
refine Function.hfunext (forall_congr fun _ ↦ propext h.mem_iff) fun h₁ h₂ _ ↦ ?_
rw [← signAux_eq_signAux2 _ _ e fun _ _ => h₁ _, ← signAux_eq_signAux2 _ _ e fun _ _ => h₂ _]
