Equiv.Perm.exists_comp_succAbove_eq_succAbove_comp_and_sign_eq
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Equiv_Perm_exists_comp_succAbove_eq_succAbove_comp_and_sign_eq
open EquivLean source · statement
theorem _root_.Equiv.Perm.exists_comp_succAbove_eq_succAbove_comp_and_sign_eq
{n : ℕ} (σ : Equiv.Perm (Fin (n + 1))) (j : Fin (n + 1)) :
∃ τ : Equiv.Perm (Fin n), (∀ k : Fin n, σ (j.succAbove k) = (σ j).succAbove (τ k)) ∧
Equiv.Perm.sign σ = (-1) ^ ((j : ℕ) + ((σ j) : ℕ)) * Equiv.Perm.sign τ