Permutations from lists of swaps

This file defines the permutations of a list of swaps and provides tactic utilities to certify row permutations of matrix literals corresponding to those swaps.

Main definitions

• permOfSwaps: the permutation swap a₀ b₀ * swap a₁ b₁ * ⋯ of a list of swaps, with its sign intCast_sign_permOfSwaps.
• mkSwapsLitQ: build the list literal of the swaps.
• certifyPermSign, certify the sign of the permutation of swaps.
• certifyPermEq: certify the row arrangement A.submatrix σ id = Aσ of a matrix literal.

def Mathlib.Tactic.Matrix.permOfSwaps {m : Type u_1} [DecidableEq m] (l : List (m × m)) : Equiv.Perm m

The permutation swap a₀ b₀ * swap a₁ b₁ * ⋯ of the swaps in l.

Equations

• Mathlib.Tactic.Matrix.permOfSwaps l = List.foldl (fun (x1 x2 : Equiv.Perm m) => x1 * x2) 1 (List.map (fun (p : m × m) => Equiv.swap p.1 p.2) l)

theorem Mathlib.Tactic.Matrix.intCast_sign_permOfSwaps {α : Type u_1} [Ring α] {m : Type u_2} [DecidableEq m] [Fintype m] {l : List (m × m)} {k : ℕ} (hl : (l.all fun (p : m × m) => p.1 != p.2) = true) (hk : l.length = k) : ↑↑(Equiv.Perm.sign (permOfSwaps l)) = (-1) ^ k

def Mathlib.Tactic.Matrix.mkSwapsLitQ (m : ℕ) (swaps : Array (ℕ × ℕ)) : Lean.MetaM Q(List (Fin «$m» × Fin «$m»))

Build the list literal of the recorded swaps, the argument of permOfSwaps.

Equations

• One or more equations did not get rendered due to their size.

def Mathlib.Tactic.Matrix.certifyPermSign {u : Lean.Level} {α : Q(Type u)} (rα : Q(CommRing «$α»)) {m : ℕ} (swaps : Q(List (Fin «$m» × Fin «$m»))) (k : ℕ) : (s : Q(«$α»)) × Q(↑↑(Equiv.Perm.sign (permOfSwaps «$swaps»)) = «$s»)

Compute the sign of the permutation of the k swaps swaps with the corresponding proof. The swaps must be between distinct rows, which an elimination guarantees.

Equations

• Mathlib.Tactic.Matrix.certifyPermSign rα swaps k = ⟨q((-1) ^ «$k»), q(⋯)⟩

def Mathlib.Tactic.Matrix.certifyPermEq {u : Lean.Level} {m n : ℕ} {α : Q(Type u)} (A Aσ : Q(Matrix (Fin «$m») (Fin «$n») «$α»)) (σ : Q(Equiv.Perm (Fin «$m»))) : Q(«$A».submatrix (⇑«$σ») id = «$Aσ»)

Prove the row arrangement A.submatrix σ id = Aσ.

Equations

• Mathlib.Tactic.Matrix.certifyPermEq A Aσ σ = Lean.Meta.mkExpectedPropHint q(⋯) q(«$A».submatrix (⇑«$σ») id = «$Aσ»)