sign_surjective — Mathlib

English

sign surjectivity: the map sign: Perm α → ℤˣ is surjective for nontrivial α.

Русский

сюръективность знака: отображение sign: Perm α → ℤˣ сюръективно для нетривиального α.

LaTeX

$$$\text{Surj}(\mathrm{sign}: \mathrm{Perm}(\alpha) \to \mathbb{Z}^\times)$$$

Lean4

theorem sign_surjective [Nontrivial α] : Function.Surjective (sign : Perm α → ℤˣ) := fun a =>
  (Int.units_eq_one_or a).elim (fun h => ⟨1, by simp [h]⟩) fun h =>
    let ⟨x, y, hxy⟩ := exists_pair_ne α
    ⟨swap x y, by rw [sign_swap hxy, h]⟩

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