Equiv.Perm.isoCycle'.proof_2
theorem Equiv.Perm.isoCycle'.proof_2 :
∀ {α : Type u_1} [inst : DecidableEq α] (s : { s // s.Nodup ∧ s.Nontrivial }), ((↑s).formPerm ⋯).IsCycle
This theorem states that for any type `α` with a decidable equality property (`DecidableEq α`), given a cycle `s` that has no duplicates (`Cycle.Nodup s`) and is made up of at least two unique elements (`Cycle.Nontrivial s`), the permutation formed from this cycle (`Cycle.formPerm ↑s`) is itself a non-identity cycle (`Equiv.Perm.IsCycle`). In other words, any nontrivial cycle without duplicates can be interpreted as a non-identity permutation in such a way that any two nonfixed points of the permutation are related by repeated application of the permutation.
More concisely: Given a decidably equal type `α` with a nontrivial, nodup cycle `s`, the permutation formed from `s` is a non-identity cycle.
|
Equiv.Perm.isoCycle'.proof_1
theorem Equiv.Perm.isoCycle'.proof_1 : ∀ {α : Type u_1} (s : { s // s.Nodup ∧ s.Nontrivial }), (↑s).Nodup
This theorem states that for any type α, if we have a cycle `s` which is a structure containing two properties - that the cycle has no duplicate elements (expressed as `Cycle.Nodup s`) and that the cycle consists of at least two unique elements (expressed as `Cycle.Nontrivial s`), then the property that the cycle has no duplicate elements (`Cycle.Nodup`) holds true for `s`. Essentially, it asserts that if a cycle is both nontrivial and contains no duplicates, then it indeed contains no duplicates.
More concisely: If a cycle is nontrivial and has no duplicate elements, then it has no duplicate elements.
|
Cycle.isCycle_formPerm
theorem Cycle.isCycle_formPerm :
∀ {α : Type u_1} [inst : DecidableEq α] (s : Cycle α) (h : s.Nodup), s.Nontrivial → (s.formPerm h).IsCycle := by
sorry
The theorem `Cycle.isCycle_formPerm` states that for any type `α` with a decidable equality relation, and a cycle `s` of `α` with the property that it has no duplicate elements (`Cycle.Nodup`), if the cycle `s` is nontrivial (meaning it contains at least two unique elements), then the permutation formed by mapping each element in the cycle to the next one (`Cycle.formPerm`) is a non-identity permutation such that any two distinct points in the permutation are related by repeated application of the permutation (`Equiv.Perm.IsCycle`).
More concisely: For any decidably equated type `α` with a non-duplicative, nontrivial cycle `s`, the permutation formed by mapping each element to the next in `s` is a non-identity cycle relation on distinct elements.
|
Equiv.Perm.toCycle_eq_toList
theorem Equiv.Perm.toCycle_eq_toList :
∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] (f : Equiv.Perm α) (hf : f.IsCycle) (x : α),
f x ≠ x → f.toCycle hf = ↑(f.toList x)
This theorem states that for a given type `α` with finite instances and a decidable equality, if `f` is a cycle permutation on `α` (meaning it is a bijection from `α` to itself where any two points which aren't fixed by the permutation are related through repeated application of the permutation), then for any element `x` of `α` which is not fixed by `f`, the cycle produced by the `toCycle` function on `f` is equivalent to the list generated by the `toList` function on `f` starting from `x`. In other words, the cycle representation of the permutation is the same as the list representation when starting from an element not fixed by the permutation.
More concisely: For a finite type `α` with decidable equality, if `f:` `α` `-->` `α` is a cycle permutation, then for any `x:` `α` not fixed by `f`, the cycle `toCycle f x` is equal to the list `toList f` starting at `x`.
|
Equiv.Perm.length_toList
theorem Equiv.Perm.length_toList :
∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] (p : Equiv.Perm α) (x : α),
(p.toList x).length = (p.cycleOf x).support.card
The theorem `Equiv.Perm.length_toList` states that for any finite type `α` with decidable equality and given any permutation `p` of `α` and any element `x` of `α`, the length of the list produced by repeatedly applying the permutation `p` to `x` until a cycle is reached, is equal to the cardinality of the set of non-fixed points of the cycle of the permutation `p` to which `x` belongs. In mathematical terms, if we denote the operation of creating a list from a permutation and a starting point as `toList`, and the operation of getting the cycle of a permutation as `cycleOf`, the theorem states that for any permutation `p` and starting point `x`, `|toList(p, x)| = |support(cycleOf(p, x))|`, where `|A|` denotes the cardinality of the set `A`.
More concisely: For any finite type `α` with decidable equality, given a permutation `p` and an element `x` of `α`, the length of the list obtained by applying `p` repeatedly to `x` until reaching a cycle equals the cardinality of the support of the cycle containing `x`.
|
Equiv.Perm.IsCycle.existsUnique_cycle_nontrivial_subtype
theorem Equiv.Perm.IsCycle.existsUnique_cycle_nontrivial_subtype :
∀ {α : Type u_1} [inst : Finite α] [inst : DecidableEq α] {f : Equiv.Perm α},
f.IsCycle → ∃! s, (↑s).formPerm ⋯ = f
This theorem states that for every type `α` that is finite and has decidable equality, if a permutation `f` on this type forms a cycle (i.e., it is a non-identity permutation where any two non-fixed points are related by repeated application of the permutation), then there exists a unique cycle `s` such that the permutation formed by `s` (given no duplicate elements) is exactly `f`. In other words, for any cyclic permutation on a finite set with decidable equality, there is a unique corresponding cycle representation.
More concisely: Given a finite type `α` with decidable equality, every cyclic permutation on `α` has a unique corresponding cycle representation.
|
List.isCycle_formPerm
theorem List.isCycle_formPerm :
∀ {α : Type u_1} [inst : DecidableEq α] {l : List α}, l.Nodup → 2 ≤ l.length → l.formPerm.IsCycle
This theorem states that for any list `l` of a type `α` (where `α` has decidable equality), if `l` has no duplicate elements (i.e., `List.Nodup l` is true) and the length of `l` is two or more (i.e., `2 ≤ List.length l`), then the permutation formed by permuting each element in `l` to the next one (i.e., `List.formPerm l`) is a cycle. In other words, the permutation is non-identity and any two non-fixed points in it are related by repeated application of the permutation.
More concisely: Given a list `l` of length greater than or equal to 2 of type `α` with decidable equality and no duplicate elements, its permutation forms a cycle.
|
Mathlib.GroupTheory.Perm.Cycle.Concrete._auxLemma.13
theorem Mathlib.GroupTheory.Perm.Cycle.Concrete._auxLemma.13 :
∀ {α : Sort u_1} {p : α → Prop} {a1 a2 : { x // p x }}, (a1 = a2) = (↑a1 = ↑a2)
This theorem, from the Mathlib library's group theory section, states that for any type `α`, any predicate `p` on `α`, and any two elements `a1` and `2` of the subtype `{ x // p x }` (i.e., the type of elements `x` satisfying `p`), `a1` and `a2` are equal if and only if their underlying elements in `α` are equal. In other words, two elements of a subtype are equal as elements of that subtype if and only if they are equal when considered as elements of the original type.
More concisely: For any type `α` and predicate `p` on `α`, elements `a1` and `a2` of the subtype `{ x // p x }` are equal if and only if their underlying elements in `α` are equal.
|