Equiv.Perm.prod_prodExtendRight
theorem Equiv.Perm.prod_prodExtendRight :
∀ {β : Type v} {α : Type u_1} [inst : DecidableEq α] (σ : α → Equiv.Perm β) {l : List α},
l.Nodup →
(∀ (a : α), a ∈ l) → (List.map (fun a => Equiv.Perm.prodExtendRight a (σ a)) l).prod = Equiv.prodCongrRight σ
The theorem `Equiv.Perm.prod_prodExtendRight` states that for any list `l` of distinct elements of type `α` (ensured by `l.Nodup`) where every element of type `α` is in this list (`∀ (a : α), a ∈ l`), if we apply the function `prodExtendRight a (σ a)` for each element `a : α`, and then combine the results using the `prod` operation, we will obtain the same result as applying `prodCongrRight σ`. Here, `σ` is a function that assigns a permutation on type `β` to every element of type `α`. The `prodExtendRight` function extends a permutation on `β` to a permutation on `α × β` by permuting the `β` coordinates that pair with a fixed `α`, while `prodCongrRight` creates an equivalence between `α × β₁` and `α × β₂` using a family of equivalences between `β₁` and `β₂` indexed by `α`.
More concisely: For any list `l` of distinct elements `α` with the property that every element `α` is in `l`, and given a permutation function `σ` from `α` to `β`, the product of `prodExtendRight a (σ a)` over all `a` in `l` equals the product obtained by applying `prodCongrRight σ`.
|
Equiv.Perm.mem_finPairsLT
theorem Equiv.Perm.mem_finPairsLT : ∀ {n : ℕ} {a : (_ : Fin n) × Fin n}, a ∈ Equiv.Perm.finPairsLT n ↔ a.snd < a.fst
The theorem `Equiv.Perm.mem_finPairsLT` states that for all natural numbers `n` and pairs `a` (consisting of elements from the set `Fin n`), the pair `a` belongs to the set `Equiv.Perm.finPairsLT n` if and only if the second element of `a` is less than the first element of `a`. In other words, it describes the membership condition for the set `Equiv.Perm.finPairsLT n` which is the set of all pairs in `Fin n` where the second component is less than the first component.
More concisely: For natural number $n$, a pair $(a, b)$ in $Fin \ n \times Fin \ n$ belongs to $Equiv.Perm.finPairsLT \ n$ if and only if $b \ < \ a$.
|
Equiv.Perm.swap_induction_on'
theorem Equiv.Perm.swap_induction_on' :
∀ {α : Type u} [inst : DecidableEq α] [inst_1 : Finite α] {P : Equiv.Perm α → Prop} (f : Equiv.Perm α),
P 1 → (∀ (f : Equiv.Perm α) (x y : α), x ≠ y → P f → P (f * Equiv.swap x y)) → P f
This theorem, `Equiv.Perm.swap_induction_on'`, establishes an induction principle for permutations. It states that given a type `α` with decidable equality and a finiteness condition, for any property `P` that applies to permutations of `α`, if `P` holds true for the identity permutation, and if `P` remains true after composing a permutation `f` with a non-trivial swap (that is, a swap between two distinct elements `x` and `y`), then `P` holds true for all permutations `f`. In terms of mathematical notation, given `P(1)` and ∀ `f, x, y` (where `x ≠ y`) `P(f) → P(f * swap(x, y))`, we can conclude ∀ `f, P(f)`.
More concisely: Given a type `α` with decidable equality and a finiteness condition, if a property `P` holds for the identity permutation and is invariant under swapping any two distinct elements, then `P` holds for all permutations of `α`.
|
Equiv.Perm.sign_permCongr
theorem Equiv.Perm.sign_permCongr :
∀ {α : Type u} [inst : DecidableEq α] {β : Type v} [inst_1 : Fintype α] [inst_2 : DecidableEq β]
[inst_3 : Fintype β] (e : α ≃ β) (p : Equiv.Perm α), Equiv.Perm.sign (e.permCongr p) = Equiv.Perm.sign p
The theorem `Equiv.Perm.sign_permCongr` states that for any types `α` and `β`, given a bijective function `e` from `α` to `β`, and any permutation `p` on `α`, the sign or parity of the permutation `p` after the bijection `e` is applied is the same as the sign or parity of the original permutation `p`. This holds if `α` and `β` have decidable equality and are finite. In other words, the signature of a permutation is invariant under the action of a bijection.
More concisely: For finite types `α` and `β` with decidable equality, if `e : α → β` is a bijective function and `p : ∣α∣! => α`, is a permutation on `α`, then the sign of `p` is equal to the sign of `e ∘ p ∘ e⁻¹`.
|
Equiv.Perm.sign_extendDomain
theorem Equiv.Perm.sign_extendDomain :
∀ {α : Type u} [inst : DecidableEq α] {β : Type v} [inst_1 : Fintype α] [inst_2 : DecidableEq β]
[inst_3 : Fintype β] (e : Equiv.Perm α) {p : β → Prop} [inst_4 : DecidablePred p] (f : α ≃ Subtype p),
Equiv.Perm.sign (e.extendDomain f) = Equiv.Perm.sign e
The theorem `Equiv.Perm.sign_extendDomain` states that for any types `α` and `β` with decidable equality, and for any finite types `α` and `β`, given a permutation `e` of `α`, a decidable predicate `p` on `β`, and a bijection `f` between `α` and the subtype of `β` that satisfies `p`, the sign or parity of the permutation obtained by extending the domain of `e` using `f` is the same as the sign of `e`. In other words, extending the domain of a permutation does not change its parity.
More concisely: For any finite types `α` and `β` with decidable equality, given a permutation `e` of `α`, a bijection `f` from `α` to a subtype of `β` satisfying a decidable predicate `p`, the sign of the permutation obtained by extending `e` using `f` equals the sign of `e`.
|
Equiv.Perm.sign_swap
theorem Equiv.Perm.sign_swap :
∀ {α : Type u} [inst : DecidableEq α] [inst_1 : Fintype α] {x y : α},
x ≠ y → Equiv.Perm.sign (Equiv.swap x y) = -1
The theorem `Equiv.Perm.sign_swap` states that for any type `α` with decidable equality and finiteness, and for any distinct elements `x` and `y` of `α`, the sign of the permutation that swaps `x` and `y` is `-1`. In other words, the permutation that merely swaps two distinct elements is considered an odd permutation.
More concisely: For any type `α` with decidable equality and finiteness, the permutation that swaps two distinct elements `x` and `y` in `α` has determinant -1.
|
Equiv.Perm.swap_induction_on
theorem Equiv.Perm.swap_induction_on :
∀ {α : Type u} [inst : DecidableEq α] [inst_1 : Finite α] {P : Equiv.Perm α → Prop} (f : Equiv.Perm α),
P 1 → (∀ (f : Equiv.Perm α) (x y : α), x ≠ y → P f → P (Equiv.swap x y * f)) → P f
This theorem provides an induction principle for permutations. It states that for any type `α` with decidable equality and finiteness, given a property `P` of permutations of `α`, if `P` is true for the identity permutation and remains true after composition with a non-trivial swap (swapping two distinct elements), then `P` is true for all permutations. In other words, we can prove a property about all permutations by proving it for the identity permutation and for the result of composing any permutation (already assumed to have the property) with a swap.
More concisely: If `P` is a property of permutations of a type `α` with decidable equality and finiteness such that `P` holds for the identity permutation and is closed under swapping distinct elements, then `P` holds for all permutations.
|
Equiv.Perm.sign_refl
theorem Equiv.Perm.sign_refl :
∀ {α : Type u} [inst : DecidableEq α] [inst_1 : Fintype α], Equiv.Perm.sign (Equiv.refl α) = 1
The theorem `Equiv.Perm.sign_refl` states that for any type `α`, which has decidable equality and is finite, the sign of the identity permutation (represented by `Equiv.refl α`) is `1`. In other words, the identity permutation is considered as an even permutation as its signature (or parity) is `1`.
More concisely: For any finite type `α` with decidable equality, the identity permutation on `α` has even signature (equivalently, its determinant is 1).
|
Equiv.Perm.sign_mul
theorem Equiv.Perm.sign_mul :
∀ {α : Type u} [inst : DecidableEq α] [inst_1 : Fintype α] (f g : Equiv.Perm α),
Equiv.Perm.sign (f * g) = Equiv.Perm.sign f * Equiv.Perm.sign g
The theorem `Equiv.Perm.sign_mul` states that for any type `α` that has decidable equality and is a finite type, and for any two permutations `f` and `g` on `α`, the signature of the product of `f` and `g` is equal to the product of the signatures of `f` and `g` individually. In other words, the sign function is multiplicative over the product of two permutations. This means that the sign of a permutation composed of two others is the product of their signs, which is essentially a property of parity: the composition of two even permutations is even, and the composition of an even and an odd permutation (in any order) is odd.
More concisely: For any finite type `α` with decidable equality, the sign of the product of two permutations on `α` is equal to the product of their individual signs.
|