Closure

📁 Source: Mathlib/GroupTheory/Perm/Closure.lean

Statistics

Metric	Count
Definitions	0
Theorems closure_cycle_adjacent_swap, closure_cycle_coprime_swap, closure_isCycle, closure_prime_cycle_swap	4
Total	4

Equiv.Perm

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
closure_cycle_adjacent_swap 📖	mathematical	IsCycle support Finset.univ	Subgroup.closure Equiv.Perm permGroup Set Set.instInsert Set.instSingletonSet Equiv.swap DFunLike.coe EquivLike.toFunLike Equiv.instEquivLike Top.top Subgroup Subgroup.instTop	—	Subgroup.subset_closure Set.mem_insert Set.mem_insert_of_mem Set.mem_singleton Equiv.mul_swap_eq_swap_mul mul_inv_cancel_right pow_succ' Subgroup.mul_mem Subgroup.inv_mem pow_zero Equiv.swap_self Subgroup.one_mem mul_apply Equiv.swap_comm Equiv.swap_mul_swap_mul_swap Finset.mem_univ IsCycle.exists_pow_eq Finite.of_fintype mem_support eq_top_iff closure_isSwap Subgroup.closure_le
closure_cycle_coprime_swap 📖	mathematical	Fintype.card IsCycle support Finset.univ	Subgroup.closure Equiv.Perm permGroup Set Set.instInsert Set.instSingletonSet Equiv.swap DFunLike.coe EquivLike.toFunLike Equiv.instEquivLike instPowNat Top.top Subgroup Subgroup.instTop	—	exists_pow_eq_self_of_coprime IsCycle.orderOf Finset.card_univ support_pow_coprime IsCycle.of_pow le_trans support_pow_le ge_of_eq eq_top_iff closure_cycle_adjacent_swap Subgroup.closure_le Set.insert_subset_iff Subgroup.pow_mem Subgroup.subset_closure Set.mem_insert Set.singleton_subset_iff Set.mem_insert_of_mem Set.mem_singleton
closure_isCycle 📖	mathematical	—	Subgroup.closure Equiv.Perm permGroup setOf IsCycle Top.top Subgroup Subgroup.instTop	—	nonempty_fintype top_le_iff le_trans ge_of_eq closure_isSwap Subgroup.closure_mono IsSwap.isCycle
closure_prime_cycle_swap 📖	mathematical	Nat.Prime Fintype.card IsCycle support Finset.univ IsSwap	Subgroup.closure Equiv.Perm permGroup Set Set.instInsert Set.instSingletonSet Top.top Subgroup Subgroup.instTop	—	IsCycle.exists_pow_eq Finite.of_fintype mem_support Finset.ext_iff Finset.mem_univ closure_cycle_coprime_swap Nat.Prime.coprime_iff_not_dvd one_apply one_pow pow_orderOf_eq_one IsCycle.orderOf Finset.card_univ pow_mul

---

← Back to Index