Equiv.Perm.IsCycleOn.isCycle_subtypePerm
theorem Equiv.Perm.IsCycleOn.isCycle_subtypePerm :
∀ {α : Type u_2} {f : Equiv.Perm α} {s : Set α} (hf : f.IsCycleOn s), s.Nontrivial → (f.subtypePerm ⋯).IsCycle := by
sorry
The theorem `Equiv.Perm.IsCycleOn.isCycle_subtypePerm` states that given any type `α`, a permutation `f` of type `Equiv.Perm α`, and a set `s` of type `α`, if `f` is a cycle on the set `s`, and if the set `s` is nontrivial (i.e., it contains at least two distinct elements), then the subtype permutation of `f` is a cycle. Here, `f.subtypePerm` refers to the permutation restricted to the subset. In the context of permutations, a cycle is a permutation which moves all elements of some subset of the type in a cyclic fashion.
More concisely: Given a nontrivial set `s` and a permutation `f` that is a cycle on `s`, the subpermission `f.subtypePerm` of `f` restricted to `s` is also a cycle.
|
Equiv.Perm.SameCycle.inv
theorem Equiv.Perm.SameCycle.inv : ∀ {α : Type u_2} {f : Equiv.Perm α} {x y : α}, f.SameCycle x y → f⁻¹.SameCycle x y
The theorem `Equiv.Perm.SameCycle.inv` states that for all types `α`, for all permutations `f` of type `α`, and for all elements `x` and `y` of type `α`, if `x` and `y` lie in the same cycle of the permutation `f`, then they also lie in the same cycle of the inverse permutation `f⁻¹`. This is an alias of the reverse direction of the theorem `Equiv.Perm.sameCycle_inv`.
More concisely: If two elements x and y belong to the same cycle of a permutation f, then they also belong to the same cycle of the inverse permutation f^-1.
|
Equiv.Perm.IsCycleOn.apply_ne
theorem Equiv.Perm.IsCycleOn.apply_ne :
∀ {α : Type u_2} {f : Equiv.Perm α} {s : Set α} {a : α}, f.IsCycleOn s → s.Nontrivial → a ∈ s → f a ≠ a
This theorem states that, for any type `α`, any permutation `f` on `α`, and any set `s` of `α`, if `f` is a cycle on `s` and `s` is a nontrivial set (i.e., `s` contains at least two distinct elements), then for every element `a` in `s`, the application of the permutation `f` to `a` does not equal `a`. In other words, in a nontrivial set on which a permutation forms a cycle, no element is mapped to itself by the permutation.
More concisely: If `f` is a permutation on a nontrivial set `s` that forms a cycle on `s`, then for all `a` in `s`, `f(a) ≠ a`.
|
Equiv.Perm.SameCycle.apply_left
theorem Equiv.Perm.SameCycle.apply_left :
∀ {α : Type u_2} {f : Equiv.Perm α} {x y : α}, f.SameCycle x y → f.SameCycle (f x) y
The theorem `Equiv.Perm.SameCycle.apply_left` is an alias for the reverse direction of `Equiv.Perm.sameCycle_apply_left`. In more descriptive terms, it states that for any type `α`, any permutation `f` of `α`, and any two elements `x` and `y` of `α`, if `x` and `y` are in the same cycle of the permutation, then the image of `x` under `f` and `y` are also in the same cycle of the permutation. In other words, if `f` cycles `x` and `y`, then `f` also cycles `f(x)` and `y`.
More concisely: If `f` is a permutation of type `α`, and `x` and `y` are elements of `α` in the same cycle of `f`, then `f(x)` and `y` are also in the same cycle of `f`.
|
Mathlib.GroupTheory.Perm.Cycle.Basic._auxLemma.1
theorem Mathlib.GroupTheory.Perm.Cycle.Basic._auxLemma.1 :
∀ {α : Type u_2} {x y : α}, Equiv.Perm.SameCycle 1 x y = (x = y)
This theorem states that for any type 'α' and any two elements 'x' and 'y' of this type, 'x' and 'y' are in the same cycle of the identity permutation if and only if 'x' equals 'y'. In the context of group theory and permutations, the identity permutation does not change any elements, thus two elements are in the same cycle of the identity permutation only when they are the same.
More concisely: For any type 'α' and any two elements 'x' and 'y' of type 'α', 'x' and 'y' are in the same cycle of the identity permutation if and only if 'x' equals 'y'. In other words, the identity permutation has only the identity element as its fixed points.
|
Mathlib.GroupTheory.Perm.Cycle.Basic._auxLemma.37
theorem Mathlib.GroupTheory.Perm.Cycle.Basic._auxLemma.37 :
∀ {F : Sort u_1} {α : Sort u_2} {β : Sort u_3} [inst : FunLike F α β] [i : EmbeddingLike F α β] (f : F) {x y : α},
(f x = f y) = (x = y)
This theorem, denoted as `Mathlib.GroupTheory.Perm.Cycle.Basic._auxLemma.37`, states that for any types `F`, `α`, and `β`, if `F` is a function-like from `α` to `β` (i.e., there is an injective coercion from `F` to the function space `α → β`) and `F` is also embedding-like from `α` to `β`, then for any function `f` of type `F` and any given elements `x` and `y` of type `α`, `f x` equals to `f y` if and only if `x` equals to `y`. In other words, it asserts that under these conditions, `f` is an injective function: it maps distinct elements of `α` to distinct elements of `β`.
More concisely: If `F` is a function-like and embedding-like from type `α` to type `β`, then the associated function `f` of type `F` is injective, i.e., `f x = f y` implies `x = y`.
|
Equiv.Perm.SameCycle.of_zpow_left
theorem Equiv.Perm.SameCycle.of_zpow_left :
∀ {α : Type u_2} {f : Equiv.Perm α} {x y : α} {n : ℤ}, f.SameCycle ((f ^ n) x) y → f.SameCycle x y
This theorem, named `Equiv.Perm.SameCycle.of_zpow_left`, states that for any type `α`, any permutation `f` of type `α`, and any elements `x` and `y` of `α`, if `y` is in the same cycle as the image of `x` under the `n`-th power of `f` (where `n` is an integer), then `y` is in the same cycle as `x`. In other words, if applying `f` `n` times to `x` results in a value that shares a cycle with `y`, then `x` and `y` are in the same cycle.
More concisely: For any permutation `f` of type `α` and integers `n` and `i` with `i` in the cycle of `x` under `f^n`, we have `x` and `i` in the same cycle under `f`.
|
Equiv.Perm.IsCycleOn.subtypePerm
theorem Equiv.Perm.IsCycleOn.subtypePerm :
∀ {α : Type u_2} {f : Equiv.Perm α} {s : Set α} (hf : f.IsCycleOn s), (f.subtypePerm ⋯).IsCycleOn Set.univ := by
sorry
This theorem states that for any type `α`, permutation `f` of `α`, and set `s` of `α`, if `f` forms a cycle on `s` (i.e., `f` is a cycle on `s`), then the permutation `f` restricted to the subset `s` (denoted by `f.subtypePerm`) is a cycle on the universal set. In other words, if a permutation has a cyclic structure when restricted to a certain set, it maintains this cyclic structure when considered over the entire universe of possible elements.
More concisely: If a permutation forms a cycle on a subset, then its restriction to that subset is a cycle on the entire domain.
|
Equiv.Perm.SameCycle.of_pow_right
theorem Equiv.Perm.SameCycle.of_pow_right :
∀ {α : Type u_2} {f : Equiv.Perm α} {x y : α} {n : ℕ}, f.SameCycle x ((f ^ n) y) → f.SameCycle x y
This theorem, referred to as an alias of the forward direction of `Equiv.Perm.sameCycle_pow_right`, states that for any type `α`, any permutation `f` of `α`, any elements `x` and `y` of `α`, and any natural number `n`, if `x` and `y` cycled by `f` to the power `n` are in the same cycle, then `x` and `y` are in the same cycle under the permutation `f`. In other words, if applying the permutation `f` `n` times to `y` results in a value that is in the same cycle as `x`, then `x` and `y` were originally in the same cycle.
More concisely: If for some permutation `f` and natural number `n`, `f^n(x)` and `x` are in the same cycle, then `x` and `x` are in the same cycle under `f`. (This statement is equivalent to the forward direction of `Equiv.Perm.sameCycle_pow_right` in Lean 4.)
|
Equiv.Perm.SameCycle.symm
theorem Equiv.Perm.SameCycle.symm : ∀ {α : Type u_2} {f : Equiv.Perm α} {x y : α}, f.SameCycle x y → f.SameCycle y x
The theorem `Equiv.Perm.SameCycle.symm` states that for any type `α` and any permutation `f` of type `α`, if two elements `x` and `y` of type `α` are in the same cycle of the permutation `f` (i.e., `Equiv.Perm.SameCycle f x y` is true), then `y` and `x` are also in the same cycle of the permutation `f` (i.e., `Equiv.Perm.SameCycle f y x` is true). In other words, the relation "being in the same cycle of a permutation" is symmetric.
More concisely: For any type `α` and permutation `f` of type `α`, if `x` and `y` are in the same cycle of `f`, then `y` and `x` are also in the same cycle of `f`. (i.e., `Equiv.Perm.SameCycle f x y` implies `Equiv.Perm.SameCycle f y x`)
|
Mathlib.GroupTheory.Perm.Cycle.Basic._auxLemma.28
theorem Mathlib.GroupTheory.Perm.Cycle.Basic._auxLemma.28 :
∀ {α : Type u_2} {f : Equiv.Perm α} {x : α}, f.SameCycle x x = True
This theorem states that for any type `α`, any permutation `f` of `α`, and any element `x` of `α`, it is always true that `x` is in the same cycle as itself under the permutation `f`. In other words, in the context of group theory, this theorem is saying that an element of a set will always belong to its own cycle when a permutation is applied. The cycle of an element under a permutation is a sequence of elements obtained by iteratively applying the permutation to the element.
More concisely: For any type `α`, any permutation `f` of `α`, and any element `x` of `α`, `x` and `f^n(x)` belong to the same cycle for some natural number `n`.
|
Equiv.Perm.SameCycle.of_inv_apply_left
theorem Equiv.Perm.SameCycle.of_inv_apply_left :
∀ {α : Type u_2} {f : Equiv.Perm α} {x y : α}, f.SameCycle (f⁻¹ x) y → f.SameCycle x y
This theorem states that for any type `α`, any permutation `f` of `α`, and any two elements `x` and `y` of `α`, if `y` is in the same cycle as the element of `α` that `f` sends `x` to, then `y` is in the same cycle as `x`. In other words, if `f` permutes `x` and `y` in such a way that they belong to the same cycle when `f` is applied inversely to `x`, then they belong to the same cycle under `f` without the inverse.
More concisely: If `x` and `y` are elements of a type `α` and are in the same cycle of a permutation `f` on `α`, then `x` and `y` belong to the same cycle under `f` without the inverse.
|
Equiv.Perm.SameCycle.trans
theorem Equiv.Perm.SameCycle.trans :
∀ {α : Type u_2} {f : Equiv.Perm α} {x y z : α}, f.SameCycle x y → f.SameCycle y z → f.SameCycle x z
The theorem `Equiv.Perm.SameCycle.trans` states that for any type `α`, for any permutation `f` of `α`, and for any elements `x`, `y`, and `z` of `α`, if `x` and `y` are in the same cycle of the permutation `f` and `y` and `z` are also in the same cycle of `f`, then `x` and `z` must be in the same cycle of `f`. This theorem captures the transitive property of the `SameCycle` relation in the context of permutations.
More concisely: If `x`, `y`, and `z` are elements of type `α` such that `x` and `y`, as well as `y` and `z`, are in the same cycle of a permutation `f` on `α`, then `x` and `z` are in the same cycle of `f`.
|
Equiv.Perm.SameCycle.of_pow_left
theorem Equiv.Perm.SameCycle.of_pow_left :
∀ {α : Type u_2} {f : Equiv.Perm α} {x y : α} {n : ℕ}, f.SameCycle ((f ^ n) x) y → f.SameCycle x y
This theorem, referred to as an alias of the forward direction of `Equiv.Perm.sameCycle_pow_left`, states that for any type `α`, permutation `f` of type `Equiv.Perm α`, and elements `x` and `y` of type `α`, and a natural number `n`, if `f` induces the same cycle for `(f^n) x` and `y`, then `f` will also induce the same cycle between `x` and `y`. In other words, raising a permutation to a power and applying it to an element does not change the cyclic behavior of the permutation with respect to that element and any other element.
More concisely: If for some permutation `f` and elements `x` and `y` of type `α`, `(f^n) x` and `y` belong to the same cycle for some natural number `n`, then `x` and `y` belong to the same cycle under `f`.
|
Equiv.Perm.SameCycle.of_apply_right
theorem Equiv.Perm.SameCycle.of_apply_right :
∀ {α : Type u_2} {f : Equiv.Perm α} {x y : α}, f.SameCycle x (f y) → f.SameCycle x y
This theorem, named "Equiv.Perm.SameCycle.of_apply_right", states that for any type `α`, any permutation `f` of type `α`, and any two elements `x` and `y` from `α`, if `x` and the result of applying `f` to `y` are in the same cycle of the permutation `f`, then `x` and `y` themselves are also in the same cycle of the permutation `f`.
More concisely: If `x` and `y` are in the same cycle of a permutation `f` on type `α`, then `x` and `y` are interchangeable by `f`. (equivalently, `f(x)` and `y` are in the same cycle of `f`)
|
Equiv.Perm.IsCycleOn.of_inv
theorem Equiv.Perm.IsCycleOn.of_inv :
∀ {α : Type u_2} {f : Equiv.Perm α} {s : Set α}, f⁻¹.IsCycleOn s → f.IsCycleOn s
The theorem `Equiv.Perm.IsCycleOn.of_inv` states that for any type `α`, any permutation `f` of type `α`, and any set `s` of type `α`, if the inverse of `f` is a cycle on `s`, then `f` is also a cycle on `s`. Here, a "cycle" refers to the property that every element of the set `s` is mapped to a unique other element in `s`, creating a cycle of elements. The theorem essentially says that if the inverse permutation creates a cycle in a set, then the original permutation also creates a cycle in that set.
More concisely: If the inverse of a permutation is a cycle on a set, then the original permutation is also a cycle on that set.
|
Equiv.Perm.IsCycle.of_pow
theorem Equiv.Perm.IsCycle.of_pow :
∀ {α : Type u_2} {f : Equiv.Perm α} [inst : DecidableEq α] [inst_1 : Fintype α] {n : ℕ},
(f ^ n).IsCycle → f.support ⊆ (f ^ n).support → f.IsCycle
This theorem states that for any type `α`, given a permutation `f` of `α`, a natural number `n`, and assuming that `α` has decidable equality and is a finite type, if the `n`-th power of `f` forms a cycle (`Equiv.Perm.IsCycle (f ^ n)`), and the set of non-fixed points of `f` is a subset of the set of non-fixed points of `f ^ n` (`Equiv.Perm.support f ⊆ Equiv.Perm.support (f ^ n)`), then `f` itself forms a cycle (`Equiv.Perm.IsCycle f`). In other words, if a permutation raised to a power forms a cycle and the non-fixed points of the original permutation are included in the non-fixed points of the powered permutation, then the original permutation is a cycle itself.
More concisely: If a permutation `f` of a finite type `α` with decidable equality forms a cycle in the `n`-th power `(f ^ n)` and the non-fixed points of `f` are a subset of those of `(f ^ n)`, then `f` itself is a cycle.
|
Equiv.Perm.sameCycle_zpow_right
theorem Equiv.Perm.sameCycle_zpow_right :
∀ {α : Type u_2} {f : Equiv.Perm α} {x y : α} {n : ℤ}, f.SameCycle x ((f ^ n) y) ↔ f.SameCycle x y
The theorem `Equiv.Perm.sameCycle_zpow_right` states that for any type `α`, any permutation `f` of `α`, and any elements `x`, `y` of `α`, and any integer `n`, `x` and `(f^n) y` are in the same cycle of the permutation `f` if and only if `x` and `y` are in the same cycle of the permutation `f`. Here, `(f^n) y` represents the result of applying the permutation `f` `n` times to `y`.
More concisely: For all types α, permutations f on α, elements x, y of α, and integers n, x and y are in the same cycle of f if and only if x and (fn) y are.
|
Equiv.Perm.IsCycle.eq_on_support_inter_nonempty_congr
theorem Equiv.Perm.IsCycle.eq_on_support_inter_nonempty_congr :
∀ {α : Type u_2} {f g : Equiv.Perm α} {x : α} [inst : DecidableEq α] [inst_1 : Fintype α],
f.IsCycle → g.IsCycle → (∀ x ∈ f.support ∩ g.support, f x = g x) → f x = g x → x ∈ f.support → f = g
The theorem `Equiv.Perm.IsCycle.eq_on_support_inter_nonempty_congr` states that for any type `α` with decidable equality and finite number of elements, if you have two cyclic permutations `f` and `g` of `α` and an element `x` of `α` such that:
- `f` and `g` are both cyclic permutations,
- for every element in the intersection of the supports of `f` and `g`, `f` and `g` map it to the same place,
- `f` and `g` map `x` to the same place,
- and `x` is in the support of `f`,
then `f` and `g` must be the same permutation. This theorem holds the importance of the intersection of supports in ensuring the identity of two cyclic permutations.
More concisely: Given finite type `α` with decidable equality, if two cyclic permutations `f` and `g` of `α` agree on the intersection of their supports and map a common support element `x` to the same image, then `f` equals `g` if `x` is in the support of `f`.
|
Mathlib.GroupTheory.Perm.Cycle.Basic._auxLemma.3
theorem Mathlib.GroupTheory.Perm.Cycle.Basic._auxLemma.3 :
∀ {α : Type u} {f : Equiv.Perm α} {x y : α}, (x = f⁻¹ y) = (f x = y)
This theorem, under the context of group theory and permutation cycles, states that for any type `α`, a permutation `f` of type `α`, and any two elements `x` and `y` of type `α`, the condition that `x` equals the inverse of `f` applied to `y` is equivalent to the condition that `f` applied to `x` equals `y`. This theorem is fundamental to the manipulation and understanding of permutations and their inverses. In mathematical terms, the theorem says that $x = f^{-1}(y)$ if and only if $f(x) = y$, for a bijective function $f$.
More concisely: For any bijective function `f` and elements `x, y` of type `α`, `x = f⁻¹(y)` if and only if `f(x) = y`.
|
Finset.product_self_eq_disjiUnion_perm
theorem Finset.product_self_eq_disjiUnion_perm :
∀ {α : Type u_2} {f : Equiv.Perm α} {s : Finset α} (hf : f.IsCycleOn ↑s),
s ×ˢ s =
(Finset.range s.card).disjiUnion (fun k => Finset.map { toFun := fun i => (i, (f ^ k) i), inj' := ⋯ } s) ⋯
This theorem states that for any given type `α`, a bijection `f : α → α` (which is a permutation on `α`), and a finite set `s : Finset α`, under the condition that `f` forms a cycle over the elements of `s`, we can partition the Cartesian product `s ×ˢ s` into disjoint union of shifted diagonals. Each diagonal is formed by mapping each element `i` of `s` to the pair `(i, (f ^ k) i)`, where `k` ranges over all natural numbers less than the cardinality of `s`. Essentially, it's saying that the square of `s` can be rearranged into a pattern of shifted diagonals, where the shifts are dictated by the permutation `f`.
More concisely: Given a finite set `s` and a bijection `f` on `s` forming a cycle, the Cartesian product `s × s` can be partitioned into disjoint shifted diagonals `{(i, (f ^ k) i) | i ∈ s, k < |s|}`.
|
Equiv.Perm.SameCycle.inv_apply_right
theorem Equiv.Perm.SameCycle.inv_apply_right :
∀ {α : Type u_2} {f : Equiv.Perm α} {x y : α}, f.SameCycle x y → f.SameCycle x (f⁻¹ y)
This theorem states that for any type `α`, given a permutation `f` of type `α`, and any two elements `x` and `y` of type `α`, if `x` and `y` are in the same cycle of the permutation `f`, then `x` and the value obtained by applying the inverse of `f` to `y` (denoted by `f⁻¹ y`) are also in the same cycle of the permutation `f`. This is essentially an alias of the theorem `Equiv.Perm.sameCycle_inv_apply_right` but in the reverse direction.
More concisely: If `x` and `y` are in the same cycle of a permutation `f`, then `x` and `f⁻¹(y)` are in the same cycle.
|
Equiv.Perm.sameCycle_comm
theorem Equiv.Perm.sameCycle_comm : ∀ {α : Type u_2} {f : Equiv.Perm α} {x y : α}, f.SameCycle x y ↔ f.SameCycle y x
This theorem states that for any type `α`, any permutation `f` on `α`, and any two elements `x` and `y` of type `α`, `x` and `y` being in the same cycle of permutation `f` is equivalent to `y` and `x` being in the same cycle of permutation `f`. In other words, the "same cycle" relation under a given permutation is symmetric: if `x` can be transformed into `y` by applying the permutation a certain number of times, then `y` can be transformed into `x` by applying the permutation a certain number of times.
More concisely: For any permutation `f` on type `α` and any `x, y` in `α`, `x` and `y` are in the same cycle of `f` if and only if `y` and `x` are in the same cycle of `f`.
|
Equiv.Perm.IsCycle.exists_zpow_eq
theorem Equiv.Perm.IsCycle.exists_zpow_eq :
∀ {α : Type u_2} {f : Equiv.Perm α} {x y : α}, f.IsCycle → f x ≠ x → f y ≠ y → ∃ i, (f ^ i) x = y
This theorem states that for any type `α`, given a permutation `f` on `α` which is a cycle (as defined by `Equiv.Perm.IsCycle`), and any two elements `x` and `y` of `α` such that `f` applied to `x` and `y` does not yield `x` and `y` respectively (`f x ≠ x` and `f y ≠ y`), there exists an integer `i` such that applying `f` to `x`, `i` times (`(f ^ i) x`), yields `y`. In other words, for a cycle permutation and two non-fixed points, you can find a number of times to apply the permutation to one point to reach the other point.
More concisely: For any cycle permutation `f` on a type `α` and distinct elements `x` and `y` in `α` with `f(x) ≠ x` and `f(y) ≠ y`, there exists an integer `i` such that `(f ^ i) x = y`.
|
Equiv.Perm.IsCycleOn.subsingleton
theorem Equiv.Perm.IsCycleOn.subsingleton : ∀ {α : Type u_2} {s : Set α}, Equiv.Perm.IsCycleOn 1 s → s.Subsingleton
The theorem `Equiv.Perm.IsCycleOn.subsingleton` states that for any given set `s` of a type `α`, if the identity permutation (represented by `1`) is a cycle on `s`, then `s` is a subsingleton set. In other words, if any two points in `s` can be related by repeated application of the identity permutation, then `s` can have at most one element. This is a specific case of the `Equiv.Perm.isCycleOn_one` theorem.
More concisely: If the identity permutation is a cycle on a set `s`, then `s` is a singleton set.
|
Equiv.Perm.SameCycle.of_inv
theorem Equiv.Perm.SameCycle.of_inv :
∀ {α : Type u_2} {f : Equiv.Perm α} {x y : α}, f⁻¹.SameCycle x y → f.SameCycle x y
This theorem is an alias for the forward direction of `Equiv.Perm.sameCycle_inv`. It states that for any type `α`, for any permutation `f` of type `α`, and for any two elements `x` and `y` of type `α`, if `x` and `y` are in the same cycle of the inverse of `f` (notated as `f⁻¹.SameCycle x y`), then `x` and `y` are also in the same cycle of `f` (denoted as `f.SameCycle x y`). Concretely, the sameCycle relation of the inverse of a permutation is equivalent to the sameCycle relation of the original permutation.
More concisely: For any permutation `f` and elements `x` and `y` of type `α`, if `x` and `y` are in the same cycle of `f⁻¹, then they are in the same cycle of `f`.
|
Equiv.Perm.IsCycle.support_pow_eq_iff
theorem Equiv.Perm.IsCycle.support_pow_eq_iff :
∀ {α : Type u_2} {f : Equiv.Perm α} [inst : DecidableEq α] [inst_1 : Fintype α],
f.IsCycle → ∀ {n : ℕ}, (f ^ n).support = f.support ↔ ¬orderOf f ∣ n
This theorem states that for any type `α` and a given permutation `f` on `α`, assuming `α` has decidable equality and is finite, if `f` is a cycle, then for any natural number `n`, the set of non-fixed points of `f^n` (that is, the points that `f^n` moves) is the same as the set of non-fixed points of `f` if and only if the order of `f` does not divide `n`. Here, the order of `f` refers to the smallest `n ≥ 1` such that `f^n` is the identity permutation, or `0` if no such `n` exists. In the context of group theory, this theorem connects the property of a permutation (being a cycle) with its algebraic property (its order).
More concisely: For any finite type `α` with decidable equality and permutation `f` that is a cycle, the sets of non-fixed points of `f` and `f^n` are equal if and only if the order of `f` does not divide `n`.
|
Equiv.Perm.IsCycleOn.inv
theorem Equiv.Perm.IsCycleOn.inv : ∀ {α : Type u_2} {f : Equiv.Perm α} {s : Set α}, f.IsCycleOn s → f⁻¹.IsCycleOn s
This theorem, `Equiv.Perm.IsCycleOn.inv`, states that for any type `α`, any permutation `f` of `α`, and any set `s` of `α`, if the permutation `f` forms a cycle on the set `s`, then the inverse permutation of `f` also forms a cycle on the same set `s`. Here, a "cycle" is a sequence of elements of the set such that applying the permutation repeatedly moves through the sequence in a cyclic manner. The inverse of a permutation is the permutation that undoes the action of the original permutation.
More concisely: If a permutation and its inverse form cycles on the same set, then the set consists of repeated applications of some finite subset.
|
Equiv.Perm.SameCycle.apply_right
theorem Equiv.Perm.SameCycle.apply_right :
∀ {α : Type u_2} {f : Equiv.Perm α} {x y : α}, f.SameCycle x y → f.SameCycle x (f y)
The theorem `Equiv.Perm.SameCycle.apply_right` states that for any type `α`, a permutation `f` of `α`, and two elements `x` and `y` of `α`, if `x` and `y` lie in the same cycle of the permutation `f`, then `x` and the image of `y` under the permutation `f` also lie in the same cycle of the permutation `f`. Essentially, this theorem explains the action of a permutation on the elements of a cycle, stating that if two elements are in the same cycle, applying the permutation to one of them keeps them in the same cycle.
More concisely: If `x` and `y` are in the same cycle of a permutation `f` on type `α`, then `x` and `f(y)` are also in the same cycle.
|
Equiv.Perm.SameCycle.pow_left
theorem Equiv.Perm.SameCycle.pow_left :
∀ {α : Type u_2} {f : Equiv.Perm α} {x y : α} {n : ℕ}, f.SameCycle x y → f.SameCycle ((f ^ n) x) y
The theorem `Equiv.Perm.SameCycle.pow_left` states that for any type `α`, any permutation `f` on `α`, and any two elements `x` and `y` of `α`, along with a natural number `n`, if `f` generates the same cycle for `x` and `y`, then the `n`th power of `f` applied to `x` also generates the same cycle with `y`. Essentially, if `x` and `y` are in the same cycle of a permutation, raising that permutation to a power and applying it to `x` keeps `x` and `y` in the same cycle.
More concisely: If permutation `f` maps `x` to `y` in the same cycle and `n` is a natural number, then `f^n(x)` maps to `f^n(y)` in the same cycle.
|
Equiv.Perm.IsCycle.sameCycle
theorem Equiv.Perm.IsCycle.sameCycle :
∀ {α : Type u_2} {f : Equiv.Perm α} {x y : α}, f.IsCycle → f x ≠ x → f y ≠ y → f.SameCycle x y
The theorem `Equiv.Perm.IsCycle.sameCycle` states that for any type `α`, and any permutation `f` of `α`, if `f` is a cycle and `f x` does not equal `x` and `f y` does not equal `y`, then `x` and `y` are in the same cycle of the permutation `f`. In other words, if a permutation `f` is a non-identity cycle, and `x` and `y` are nonfixed points under `f`, then there exists some integer `i` such that applying `f` `i` times to `x` gives `y`.
More concisely: If `f` is a non-identity cycle permutation on type `α`, and `x` and `y` are distinct points not fixed by `f`, then there exists an integer `i` such that `f^i(x) = y`.
|
Equiv.Perm.sameCycle_apply_right
theorem Equiv.Perm.sameCycle_apply_right :
∀ {α : Type u_2} {f : Equiv.Perm α} {x y : α}, f.SameCycle x (f y) ↔ f.SameCycle x y
This theorem states that for any type `α`, for any permutation `f` of `α`, and for any elements `x` and `y` of `α`, `x` and `f(y)` are in the same cycle of `f` if and only if `x` and `y` are in the same cycle of `f`. In other words, applying the permutation `f` to `y` does not change whether `x` and `y` are in the same cycle of `f`.
More concisely: For any permutation `f` and elements `x` and `y` of type `α`, `x` and `y` are in the same cycle of `f` if and only if `f(y)` is in the same cycle of `x`.
|
Equiv.Perm.isCycle_iff_exists_isCycleOn
theorem Equiv.Perm.isCycle_iff_exists_isCycleOn :
∀ {α : Type u_2} {f : Equiv.Perm α},
f.IsCycle ↔ ∃ s, s.Nontrivial ∧ f.IsCycleOn s ∧ ∀ ⦃x : α⦄, ¬Function.IsFixedPt (⇑f) x → x ∈ s
This theorem describes a relationship between two properties of a permutation of a type `α`: being a cycle (`IsCycle`) and having a nontrivial subset on which it is a cycle (`IsCycleOn`). Specifically, it states that for any permutation `f` of a type `α`, `f` is a cycle if and only if there exists a nontrivial subset `s` of `α` such that `f` is a cycle on `s`, and for all elements `x` of `α`, if `x` is not a fixed point of `f`, then `x` is in `s`. In other words, a permutation is a cycle if it is a cycle on some nontrivial subset, and all of its non-fixed points are in that subset.
More concisely: A permutation on a type `α` is a cycle if and only if there exists a nontrivial subset `s` such that it is a cycle on `s` and maps all non-fixed points to `s`.
|
Equiv.Perm.IsCycle.orderOf
theorem Equiv.Perm.IsCycle.orderOf :
∀ {α : Type u_2} {f : Equiv.Perm α} [inst : DecidableEq α] [inst_1 : Fintype α],
f.IsCycle → orderOf f = f.support.card
This theorem states that for any type `α`, given a permutation `f` of `α` which forms a cycle, the order of `f` (i.e., the smallest positive integer `n` such that `f^n` is the identity function, if such an `n` exists, otherwise `0`) is equal to the number of elements in the `f`'s support set. The support set of a permutation is the set of points not fixed by the permutation. This holds true when `α` has decidable equality and is a finite type.
More concisely: For any finite type `α` with decidable equality, the order of a permutation `f` on `α` equals the cardinality of its support set.
|
Equiv.Perm.SameCycle.refl
theorem Equiv.Perm.SameCycle.refl : ∀ {α : Type u_2} (f : Equiv.Perm α) (x : α), f.SameCycle x x
This theorem states that for any type `α`, any permutation `f` of `α`, and any element `x` of `α`, `x` is in the same cycle as itself under the permutation `f`. In other words, for any element and any permutation, there exists some integer `i` such that applying the permutation `f` `i` times to `x` returns `x` itself. This is a reflexivity property of the `SameCycle` relation for permutations.
More concisely: For any permutation `f` and element `x` in a type `α`, `x` is in the same cycle as `x` under `f`. (Or, more formally, for all `α`, `f: α → α`, and `x: α`, `SameCycle f x x` holds in Lean.)
|
Equiv.Perm.IsCycle.support_congr
theorem Equiv.Perm.IsCycle.support_congr :
∀ {α : Type u_2} {f g : Equiv.Perm α} [inst : DecidableEq α] [inst_1 : Fintype α],
f.IsCycle → g.IsCycle → f.support ⊆ g.support → (∀ x ∈ f.support, f x = g x) → f = g
The theorem `Equiv.Perm.IsCycle.support_congr` states that for any type `α`, and for any two permutations `f` and `g` of `α`, given that `α` has a decidable equality and is a finite type, if `f` is a cycle, `g` is also a cycle, the support of `f` is a subset of the support of `g`, and for every element `x` in the support of `f`, we have `f(x) = g(x)`, then `f` is equal to `g`. In other words, two cyclic permutations are equal if they act the same on the support of the smaller one.
More concisely: If `α` is a finite type with decidable equality, `f` and `g` are cyclic permutations of `α`, and the support of `f` is subset of the support of `g` with `f(x) = g(x)` for all `x` in the support of `f`, then `f = g`.
|
Equiv.Perm.SameCycle.subtypePerm
theorem Equiv.Perm.SameCycle.subtypePerm :
∀ {α : Type u_2} {f : Equiv.Perm α} {p : α → Prop} {h : ∀ (x : α), p x ↔ p (f x)} {x y : { x // p x }},
f.SameCycle ↑x ↑y → (f.subtypePerm h).SameCycle x y
This theorem, named `Equiv.Perm.SameCycle.subtypePerm`, is about the notion of permutations on a type `α` and a property `p` defined on `α`. Specifically, it says that given any type `α`, any permutation `f` on `α`, and any property `p` such that `p` remains invariant under `f` (i.e., for any element `x` of `α`, `p(x)` is true if and only if `p(f(x))` is true), if `x` and `y` are elements of the subtype of `α` consisting of elements satisfying `p`, and `x` and `y` lie in the same cycle of `f`, then they also lie in the same cycle of the permutation `f.subtypePerm(h)`, which is the restriction of `f` to the subtype `{x // p x}`.
More concisely: Given a permutation `f` on type `α` preserving property `p`, if `x` and `y` in the subtype `{x : α | p x}` lie in the same cycle of `f`, then they also lie in the same cycle of `f.subtypePerm(h)`, the restriction of `f` to this subtype.
|
Equiv.Perm.SameCycle.extendDomain
theorem Equiv.Perm.SameCycle.extendDomain :
∀ {α : Type u_2} {β : Type u_3} {g : Equiv.Perm α} {x y : α} {p : β → Prop} [inst : DecidablePred p]
{f : α ≃ Subtype p}, g.SameCycle x y → (g.extendDomain f).SameCycle ↑(f x) ↑(f y)
The theorem `Equiv.Perm.SameCycle.extendDomain` states that for any types `α` and `β`, a permutation `g` on `α`, two elements `x` and `y` of `α`, a decidable predicate `p` on `β`, and an equivalence `f` between `α` and the subtype of `β` satisfying `p`, if `x` and `y` are in the same cycle of the permutation `g`, then the elements `f(x)` and `f(y)` are also in the same cycle of the permutation `g` extended to the domain `β` by the equivalence `f`. This theorem is an alias of the reverse direction of `Equiv.Perm.sameCycle_extendDomain`.
More concisely: Given types `α`, `β`, a permutation `g` on `α`, an equivalence `f : α ≃ subtype p of β`, and `x`, `y` in `α` in the same cycle of `g`, the elements `f(x)` and `f(y)` are also in the same cycle of `g` extended to `β` via `f`.
|
Equiv.Perm.SameCycle.inv_apply_left
theorem Equiv.Perm.SameCycle.inv_apply_left :
∀ {α : Type u_2} {f : Equiv.Perm α} {x y : α}, f.SameCycle x y → f.SameCycle (f⁻¹ x) y
The theorem `Equiv.Perm.SameCycle.inv_apply_left` states that for any type `α`, any permutation `f` of `α`, and any two elements `x` and `y` of `α`, if `x` and `y` belong to the same cycle under the permutation `f`, then the image of `x` under the inverse of `f`, denoted by `f⁻¹ x`, also belongs to the same cycle as `y` under the permutation `f`. In other words, if `x` and `y` are in the same cycle of a permutation, then applying the inverse of that permutation to `x` results in an element that is in the same cycle as `y`.
More concisely: If `x` and `y` are in the same cycle of a permutation `f`, then `f⁻¹ x` is also in that cycle.
|
Mathlib.GroupTheory.Perm.Cycle.Basic._auxLemma.24
theorem Mathlib.GroupTheory.Perm.Cycle.Basic._auxLemma.24 :
∀ {α : Type u_1} {β : Type u_2} (f : α → β), Set.BijOn f ∅ ∅ = True
This theorem states that for all types `α` and `β`, and for any function `f` from `α` to `β`, the function `f` is bijective on the empty set to the empty set. In other words, for any function `f`, it is true that `f` maps every element of the empty set to a unique element of the empty set (which is vacuously true, as the empty set has no elements), `f` is injective on the empty set (meaning that distinct elements of the empty set map to distinct elements in the image, again vacuously true), and `f` is surjective on the empty set (meaning that every element of the empty set is the image of an element of the empty set under `f`, also vacuously true).
More concisely: The empty function is bijective between any two empty sets.
|
Equiv.Perm.SameCycle.of_apply_left
theorem Equiv.Perm.SameCycle.of_apply_left :
∀ {α : Type u_2} {f : Equiv.Perm α} {x y : α}, f.SameCycle (f x) y → f.SameCycle x y
The theorem `Equiv.Perm.SameCycle.of_apply_left` states that for any type `α`, permutation `f` of type `α` and any two elements `x` and `y` of `α`, if `f` maps to the same cycle when applied to `x` and `y`, then `x` and `y` are also in the same cycle of `f`. In other words, if applying the permutation `f` to `x` results in the same cycle as `y`, then `x` and `y` are in the same cycle under the permutation `f`.
More concisely: If two elements have the same cycle under a permutation, then they belong to the same cycle.
|
Equiv.Perm.sameCycle_apply_left
theorem Equiv.Perm.sameCycle_apply_left :
∀ {α : Type u_2} {f : Equiv.Perm α} {x y : α}, f.SameCycle (f x) y ↔ f.SameCycle x y
The theorem `Equiv.Perm.sameCycle_apply_left` states that for any type `α`, any permutation `f` of `α`, and any two elements `x` and `y` of `α`, `x` and `y` are in the same cycle of the permutation `f` if and only if the image of `x` under `f` and `y` are also in the same cycle of `f`. In other words, applying the permutation `f` to `x` does not change whether it is in the same cycle as `y` under the permutation `f`.
More concisely: For any type `α`, permutation `f` of `α`, and elements `x` and `y` of `α`, `x` and `y` are in the same cycle of `f` if and only if `f(x)` and `y` are in the same cycle of `f`.
|
Mathlib.GroupTheory.Perm.Cycle.Basic._auxLemma.2
theorem Mathlib.GroupTheory.Perm.Cycle.Basic._auxLemma.2 :
∀ {α : Type u_2} {f : Equiv.Perm α} {x y : α}, f⁻¹.SameCycle x y = f.SameCycle x y
This theorem states that for any type `α`, any permutation `f` on `α`, and any two elements `x` and `y` of `α`, `x` and `y` are in the same cycle of the inverse permutation `f⁻¹` if and only if they are in the same cycle of the permutation `f`. In other words, being in the same cycle is an invariant property under taking the inverse of a permutation.
More concisely: For any permutation `f` on type `α`, elements `x` and `y` are in the same cycle of `f` if and only if they are in the same cycle of `f⁻¹`.
|
Equiv.Perm.sameCycle_zpow_left
theorem Equiv.Perm.sameCycle_zpow_left :
∀ {α : Type u_2} {f : Equiv.Perm α} {x y : α} {n : ℤ}, f.SameCycle ((f ^ n) x) y ↔ f.SameCycle x y
The theorem `Equiv.Perm.sameCycle_zpow_left` states that for any given permutation `f` of a type `α`, and any two elements `x` and `y` of type `α`, as well as an integer `n`, the statement that `y` is in the same cycle of the permutation `f` as `f^n(x)` is equivalent to the statement that `y` is in the same cycle as `x`. Here `f^n(x)` denotes applying the permutation `f` `n` times to `x`. In other words, applying a permutation multiple times to a point doesn't change the cycle that the point belongs to.
More concisely: For any permutation `f` on type `α` and elements `x, y` of type `α`, if `x` and `y` are in the same cycle of `f`, then `y` is in the same cycle as `f^n(x)` for any integer `n`.
|
Equiv.Perm.SameCycle.pow_right
theorem Equiv.Perm.SameCycle.pow_right :
∀ {α : Type u_2} {f : Equiv.Perm α} {x y : α} {n : ℕ}, f.SameCycle x y → f.SameCycle x ((f ^ n) y)
This theorem, known as the "Alias of the reverse direction of `Equiv.Perm.sameCycle_pow_right`", states that for any type `α`, any bijection `f` from `α` to `α`, any elements `x` and `y` of `α`, and any natural number `n`, if `x` and `y` are in the same cycle of the permutation `f`, then `x` and `f^n(y)` (the application of `f` to `y`, `n` times) are also in the same cycle of the permutation `f`.
More concisely: If `x` and `y` are in the same cycle of a bijection `f` from `α` to `α`, then `x` and `f^n(y)` are in the same cycle for any natural number `n`.
|
Equiv.Perm.SameCycle.zpow_left
theorem Equiv.Perm.SameCycle.zpow_left :
∀ {α : Type u_2} {f : Equiv.Perm α} {x y : α} {n : ℤ}, f.SameCycle x y → f.SameCycle ((f ^ n) x) y
The theorem `Equiv.Perm.SameCycle.zpow_left` states that for any type `α`, permutation `f` of type `α`, and elements `x` and `y` of type `α`, as well as an integer `n`, if `f` maps `x` to `y` in the same cycle, then raising `f` to the power `n` and applying the result to `x` also results in an element that is in the same cycle as `y`. More simply, it means that if `x` and `y` are in the same cycle under a permutation, then any power of this permutation keeps `x` and `y` in the same cycle.
More concisely: If permutation `f` maps elements `x` and `y` to each other in the same cycle, then raising `f` to the power `n` maps `x` to an element in the same cycle as `y` for all integers `n`.
|
Equiv.Perm.SameCycle.rfl
theorem Equiv.Perm.SameCycle.rfl : ∀ {α : Type u_2} {f : Equiv.Perm α} {x : α}, f.SameCycle x x
This theorem states that for any type `α`, any permutation `f` of `α`, and any element `x` from `α`, `x` is in the same cycle of the permutation `f` as itself. In other words, `x` will always be part of its own cycle in any given permutation.
More concisely: For any type `α`, any permutation `f` on `α`, and any element `x` in `α`, `x` and `f(x)` belong to the same cycle in the cycle decomposition of `f`.
|
Equiv.Perm.SameCycle.of_inv_apply_right
theorem Equiv.Perm.SameCycle.of_inv_apply_right :
∀ {α : Type u_2} {f : Equiv.Perm α} {x y : α}, f.SameCycle x (f⁻¹ y) → f.SameCycle x y
This theorem, called "SameCycle.of_inv_apply_right", states that for any type `α`, any permutation `f` of type `α`, and any two elements `x` and `y` of type `α`, if `x` and the inverse of `f` applied to `y` are in the same cycle of the permutation `f`, then `x` and `y` are also in the same cycle of the permutation `f`. In other words, it asserts the equivalence of `f.SameCycle x (f⁻¹ y)` and `f.SameCycle x y` under certain conditions.
More concisely: If `x` and `y` are elements of type `α`, and `f` is a permutation of type `α`, then `x` and `y` are in the same cycle of `f` if and only if they are in the same cycle of the inverse of `f`.
|
Set.Subsingleton.isCycleOn_one
theorem Set.Subsingleton.isCycleOn_one : ∀ {α : Type u_2} {s : Set α}, s.Subsingleton → Equiv.Perm.IsCycleOn 1 s := by
sorry
This theorem, referred to as `Set.Subsingleton.isCycleOn_one`, states that for any type `α` and any set `s` of type `α`, if `s` is a subsingleton set (i.e., a set with at most one element), then the identity permutation is considered a cycle on `s`. This is evidenced by the fact that any two points of `s` are related by repeated application of the identity permutation. It's an alias of the reverse direction of `Equiv.Perm.isCycleOn_one`.
More concisely: If `s` is a subsingleton set, then the identity permutation is a cycle on `s`.
|
Equiv.Perm.IsCycle.inv
theorem Equiv.Perm.IsCycle.inv : ∀ {α : Type u_2} {f : Equiv.Perm α}, f.IsCycle → f⁻¹.IsCycle
The theorem `Equiv.Perm.IsCycle.inv` states that for all types `α` and any permutation `f` of type `α`, if `f` is a cycle (i.e., it's a non-identity permutation where any two nonfixed points are related by repeated application of the permutation), then the inverse of `f` is also a cycle. This theorem, in essence, proposes that the cycle property is preserved under the operation of inversion.
More concisely: If `f` is a cycle permution of type `α`, then the inverse `f⁻¹` is also a cycle.
|
Equiv.Perm.SameCycle.apply_eq_self_iff
theorem Equiv.Perm.SameCycle.apply_eq_self_iff :
∀ {α : Type u_2} {f : Equiv.Perm α} {x y : α}, f.SameCycle x y → (f x = x ↔ f y = y)
This theorem states that for any type `α`, any permutation `f` on `α`, and any two elements `x` and `y` of `α`, if `x` and `y` are in the same cycle of the permutation `f` (i.e., there exists a integer `i` such that applying the permutation `f` `i` times to `x` yields `y`), then `x` being a fixed point of `f` (meaning `f(x) = x`) is equivalent to `y` being a fixed point of `f` (meaning `f(y) = y`). In other words, either both `x` and `y` are fixed points of `f` or neither of them are.
More concisely: For any permutation `f` on a type `α` and any elements `x` and `y` in `α`, if `x` and `y` are in the same cycle of `f`, then `x` being a fixed point of `f` if and only if `y` is a fixed point of `f`.
|
Mathlib.GroupTheory.Perm.Cycle.Basic._auxLemma.41
theorem Mathlib.GroupTheory.Perm.Cycle.Basic._auxLemma.41 :
∀ {α : Type u_1} {a : α} {s : Finset α}, (a ∈ ↑s) = (a ∈ s)
This theorem is part of the `Mathlib.GroupTheory.Perm.Cycle.Basic` in Lean 4 and is named `_auxLemma.41`. It states that for any types `α` and `β`, a function `f` from `α` to `β`, a set `s` of type `α`, and an element `y` of type `β`, the property of `y` being in the image of set `s` under the function `f` (denoted as `y ∈ f '' s`) is equivalent to the existence of an element `x` in the set `s` such that `f` applied to `x` yields `y` (denoted as `∃ x ∈ s, f x = y`). Essentially, it provides a characterization of the image of a set under a function.
More concisely: For any types α and β, a function f from α to β, and a set s of type α, the image of s under f (y ∈ f '' s) if and only if there exists an x in s such that f(x) = y.
|
Equiv.Perm.IsCycle.ne_one
theorem Equiv.Perm.IsCycle.ne_one : ∀ {α : Type u_2} {f : Equiv.Perm α}, f.IsCycle → f ≠ 1
The theorem `Equiv.Perm.IsCycle.ne_one` states that for any type `α` and any permutation `f` of type `α`, if `f` is a cycle (i.e., a non-identity permutation where any two non-fixed points are related by repeated application of the permutation), then `f` is not equal to the identity permutation (denoted as `1`). In other words, a cyclic permutation is never the identity.
More concisely: For any type `α` and permutation `f` of type `α`, if `f` is a cycle, then `f ≠ 1`.
|
Equiv.Perm.SameCycle.of_zpow_right
theorem Equiv.Perm.SameCycle.of_zpow_right :
∀ {α : Type u_2} {f : Equiv.Perm α} {x y : α} {n : ℤ}, f.SameCycle x ((f ^ n) y) → f.SameCycle x y
The theorem `Equiv.Perm.SameCycle.of_zpow_right` states that for any type `α`, any permutation `f` of `α`, and any elements `x` and `y` of `α`, if `x` and `y` are in the same cycle under `f` raised to some integer power `n`, then `x` and `y` are in the same cycle under `f`. In other words, if applying the permutation `f` repeatedly `n` times, cycles `x` and `y` together, then they are also cycled together by the original permutation `f`.
More concisely: If `x` and `y` are in the same cycle under the power `n` of a permutation `f` on type `α`, then they are in the same cycle under `f`.
|
Equiv.Perm.SameCycle.zpow_right
theorem Equiv.Perm.SameCycle.zpow_right :
∀ {α : Type u_2} {f : Equiv.Perm α} {x y : α} {n : ℤ}, f.SameCycle x y → f.SameCycle x ((f ^ n) y)
This theorem, named `Equiv.Perm.SameCycle.zpow_right`, specifies that for any type `α`, for any permutation `f` of `α`, for any elements `x` and `y` of `α`, and for any integer `n`, if `f` cycles `x` and `y` in the same way, then `f` will also cycle `x` and the `n`-th power of `f` applied to `y` in the same way. In simpler terms, if a permutation leads `x` and `y` to follow the same cycle, then the same permutation will lead `x` to follow the same cycle as `y` after `n` applications of the permutation.
More concisely: If two elements are in the same cycle of a permutation, then they are in the same cycle of every power of that permutation.
|