Equiv.Perm.IsThreeCycle.cycleType
theorem Equiv.Perm.IsThreeCycle.cycleType :
∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] {σ : Equiv.Perm α},
σ.IsThreeCycle → σ.cycleType = {3}
This theorem states that for any type 'α' that has a finite number of elements ('Fintype α') and has a decidable equality ('DecidableEq α'), if a permutation 'σ' is a three-cycle (meaning it is a cycle of length 3, as defined by 'Equiv.Perm.IsThreeCycle'), then the cycle type of this permutation (which is given by 'Equiv.Perm.cycleType σ') is equal to the singleton Multiset containing only the number 3. In simple terms, this theorem confirms that a three-cycle permutation has a cycle type of {3}.
More concisely: For any finite type 'α' with decidable equality, a three-cycle permutation in its permutation group has a cycle type equal to the singleton set {3}.
|
exists_prime_orderOf_dvd_card
theorem exists_prime_orderOf_dvd_card :
∀ {G : Type u_3} [inst : Group G] [inst_1 : Fintype G] (p : ℕ) [hp : Fact p.Prime],
p ∣ Fintype.card G → ∃ x, orderOf x = p
The theorem `exists_prime_orderOf_dvd_card` states that for any prime number `p` that divides the order (i.e., number of elements) of a finite group `G`, there exists an element in `G` whose order is `p`. This is known as Cauchy's theorem in group theory. In other words, if the size of a finite group is divisible by a prime number, then the group contains an element of which the order is equal to that prime number.
More concisely: For any prime number `p` that divides the order of a finite group `G`, there exists an element in `G` with order `p`.
|
Equiv.Perm.card_fixedPoints_modEq
theorem Equiv.Perm.card_fixedPoints_modEq :
∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] {f : Function.End α} {p n : ℕ} [hp : Fact p.Prime],
f ^ p ^ n = 1 → p.ModEq (Fintype.card α) (Fintype.card ↑(Function.fixedPoints f))
The theorem `Equiv.Perm.card_fixedPoints_modEq` states that for any finite type `α` with a decidable equality relation, given a function `f` which is an endomorphism on `α`, and given `p` and `n` as natural numbers where `p` is a prime number, if `f` raised to the power of `p` to the power of `n` results in the identity function, then the number of fixed points of `f` and the total number of elements in `α` are congruent modulo `p`. In other words, when you divide the total number of elements in `α` and the number of fixed points of `f` by the prime number `p`, the remainders are the same.
More concisely: If `f` is an endomorphism of a finite type `α` with decidable equality and `p` is a prime number, then the number of fixed points of `f` is congruent to the total number of elements in `α` modulo `p`, if `f^(p^n)` is the identity function.
|
Equiv.Perm.one_lt_of_mem_cycleType
theorem Equiv.Perm.one_lt_of_mem_cycleType :
∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] {σ : Equiv.Perm α} {n : ℕ}, n ∈ σ.cycleType → 1 < n
The theorem `Equiv.Perm.one_lt_of_mem_cycleType` states that for any given finite type `α` with decidable equality, for any permutation `σ` of `α`, and for any natural number `n`, if `n` is a member of the cycle type of the permutation `σ`, then `n` is greater than 1. In other words, all cycle lengths in the cycle type of a permutation are greater than 1.
More concisely: For any finite type with decidable equality and any permutation of it, all cycle lengths in its cycle type are greater than 1.
|
Equiv.Perm.sum_cycleType
theorem Equiv.Perm.sum_cycleType :
∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] (σ : Equiv.Perm α), σ.cycleType.sum = σ.support.card
This theorem states that for any finite type `α` with decidable equality and any permutation `σ` of this type, the sum of the cycle type of the permutation (which is a multiset of natural numbers representing the lengths of the cycles in the permutation) is equal to the cardinality of the set of non-fixed points (elements that are not mapped to themselves) of the permutation. In other words, if you break a permutation down into its cycles, sum the lengths of those cycles, and compare this sum to the total number of elements in the permutation that are moved, these two numbers will always be equal.
More concisely: For any finite type with decidable equality, the sum of the cycle lengths of a permutation equals the number of its non-fixed points.
|
Equiv.Perm.Disjoint.cycleType
theorem Equiv.Perm.Disjoint.cycleType :
∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] {σ τ : Equiv.Perm α},
σ.Disjoint τ → (σ * τ).cycleType = σ.cycleType + τ.cycleType
The theorem `Equiv.Perm.Disjoint.cycleType` states that for any finite type `α` equipped with a decidable equality and any two disjoint permutations `σ` and `τ` over `α`, the cycle type of the product of `σ` and `τ` is the sum of the cycle types of `σ` and `τ`. In other words, if `σ` and `τ` are permutations on `α` such that every element is fixed by either `σ` or `τ` but not both (i.e., they are disjoint), then the structure of cycles (as given by their lengths) in the permutation resulting from their composition (the action of `τ` followed by `σ`) is the same as the combined structures of the cycles in `σ` and `τ`.
More concisely: For any finite type equipped with decidable equality, the cycle types of two disjoint permutations sum to the cycle type of their composition.
|
Equiv.Perm.two_le_of_mem_cycleType
theorem Equiv.Perm.two_le_of_mem_cycleType :
∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] {σ : Equiv.Perm α} {n : ℕ}, n ∈ σ.cycleType → 2 ≤ n
This theorem states that for any given type `α` (which is finite and has a decidable equality), any permutation `σ` of `α`, and any natural number `n`, if `n` is a member of the cycle type of the permutation `σ`, then `n` must be greater than or equal to 2. In mathematical terms, the cycle type of a permutation `σ` is a multiset of nonnegative integers, and this theorem asserts that every integer in this multiset is at least 2.
More concisely: For any finite type `α` with decidable equality, if `σ` is a permutation of `α` and `n` is a cycle length of `σ`, then `n` ≥ 2.
|
exists_prime_addOrderOf_dvd_card
theorem exists_prime_addOrderOf_dvd_card :
∀ {G : Type u_3} [inst : AddGroup G] [inst_1 : Fintype G] (p : ℕ) [hp : Fact p.Prime],
p ∣ Fintype.card G → ∃ x, addOrderOf x = p
The theorem `exists_prime_addOrderOf_dvd_card` states that for any prime number `p` that divides the order (or total number of elements) of a finite additive group `G`, there exists an element in `G` whose order is `p`. This is an additive version of Cauchy's theorem. In mathematical terms, if `p` is a prime number that divides the cardinality of a finite additive group `G`, then there exists an element `x` in `G` such that the smallest positive integer `n` for which `n` times `x` equals the additive identity (zero) is `p`.
More concisely: If a prime number `p` divides the order of a finite additive group `G`, then `G` contains an element of order `p`.
|
Equiv.Perm.dvd_of_mem_cycleType
theorem Equiv.Perm.dvd_of_mem_cycleType :
∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] {σ : Equiv.Perm α} {n : ℕ},
n ∈ σ.cycleType → n ∣ orderOf σ
The theorem `Equiv.Perm.dvd_of_mem_cycleType` asserts that for any finite type `α` with decidable equality and any permutation `σ` over `α`, if a natural number `n` belongs to the cycle type of `σ`, then `n` divides the order of `σ`. Here, the cycle type of a permutation is represented as a multiset of natural numbers, where each number corresponds to the size of a cycle in the permutation. The order of a permutation is defined as the smallest positive integer `n` such that applying the permutation `n` times is equivalent to doing nothing, or in other words, `σ^n = 1`. If such `n` does not exist, the order of the permutation is defined to be `0`.
More concisely: If `σ` is a permutation on a finite type `α` with decidable equality, and `n` is in the cycle type of `σ`, then `n` divides the order of `σ`.
|
Equiv.Perm.IsCycle.cycleType
theorem Equiv.Perm.IsCycle.cycleType :
∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] {σ : Equiv.Perm α},
σ.IsCycle → σ.cycleType = ↑[σ.support.card]
The theorem `Equiv.Perm.IsCycle.cycleType` states that for any finite type `α` with decidable equality and any permutation `σ` on `α`, if `σ` is a cycle (i.e., a non-identity permutation where any two non-fixed points of the permutation are related by repeated application of the permutation), then the cycle type of `σ` (i.e., the multiset of the sizes of the orbits of `σ`) is a singleton multiset containing the cardinality of the support of `σ` (i.e., the set of non-fixed points of `σ`). In other words, if `σ` is a cycle, then there is exactly one orbit of non-fixed points, and its size is the number of non-fixed points.
More concisely: If `σ` is a finite permutation on a type `α` with decidable equality, then `σ` being a cycle implies the cycle type of `σ` is a singleton multiset containing the cardinality of `σ`'s support.
|
Equiv.Perm.cycleType_def
theorem Equiv.Perm.cycleType_def :
∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] (σ : Equiv.Perm α),
σ.cycleType = Multiset.map (Finset.card ∘ Equiv.Perm.support) σ.cycleFactorsFinset.val
The theorem `Equiv.Perm.cycleType_def` states that for any type `α` with decidable equality and finiteness, and for any permutation `σ` on `α`, the cycle type of `σ` is defined as the multiset obtained by mapping each element of the finset of cycle factors of `σ` to its cardinality (the number of elements in the set), computed over the set of non-fixed points of the respective cycle. In simple terms, it calculates the size of each cycle in a permutation, and returns a multiset of these sizes.
More concisely: Given a type `α` with decidable equality and finiteness, and a permutation `σ` on `α`, the cycle type of `σ` is the multiset of sizes of its cycles, where each cycle is considered as a subset of the non-fixed points of the cycle.
|
Equiv.Perm.cycleType_one
theorem Equiv.Perm.cycleType_one :
∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α], Equiv.Perm.cycleType 1 = 0
The theorem `Equiv.Perm.cycleType_one` states that for any finite type `α` with decidable equality, the cycle type of the identity permutation is zero. In other words, the number of cycles of each length in the decomposition of the identity permutation into disjoint cycles, which is represented as a multiset of natural numbers, is zero for any given finite type with decidable equality.
More concisely: The identity permutation on a finite type with decidable equality has no cycles.
|