Basic

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

Statistics

Metric	Count
Definitions	0
Theorems swap_smul_involutive, swap_smul_self_smul, perm_inv, perm_pow, perm_zpow, perm_pow, perm_pow	7
Total	7

Equiv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
swap_smul_involutive 📖	mathematical	—	Function.Involutive Perm SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid Perm.permGroup MulAction.toSemigroupAction swap	—	swap_smul_self_smul
swap_smul_self_smul 📖	mathematical	—	Perm SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid Perm.permGroup MulAction.toSemigroupAction swap	—	smul_smul swap_mul_self one_smul

Set.BijOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
perm_inv 📖	mathematical	Set.BijOn DFunLike.coe Equiv.Perm EquivLike.toFunLike Equiv.instEquivLike	Set.BijOn DFunLike.coe Equiv.Perm EquivLike.toFunLike Equiv.instEquivLike Equiv.Perm.instInv	—	symm Equiv.invOn
perm_pow 📖	mathematical	Set.BijOn DFunLike.coe Equiv.Perm EquivLike.toFunLike Equiv.instEquivLike	Set.BijOn DFunLike.coe Equiv.Perm EquivLike.toFunLike Equiv.instEquivLike Equiv.Perm.instPowNat	—	iterate
perm_zpow 📖	mathematical	Set.BijOn DFunLike.coe Equiv.Perm EquivLike.toFunLike Equiv.instEquivLike	Set.BijOn DFunLike.coe Equiv.Perm EquivLike.toFunLike Equiv.instEquivLike DivInvMonoid.toZPow Group.toDivInvMonoid Equiv.Perm.permGroup	—	perm_pow perm_inv

Set.MapsTo

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
perm_pow 📖	mathematical	Set.MapsTo DFunLike.coe Equiv.Perm EquivLike.toFunLike Equiv.instEquivLike	Set.MapsTo DFunLike.coe Equiv.Perm EquivLike.toFunLike Equiv.instEquivLike Equiv.Perm.instPowNat	—	iterate

Set.SurjOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
perm_pow 📖	mathematical	Set.SurjOn DFunLike.coe Equiv.Perm EquivLike.toFunLike Equiv.instEquivLike	Set.SurjOn DFunLike.coe Equiv.Perm EquivLike.toFunLike Equiv.instEquivLike Equiv.Perm.instPowNat	—	iterate

---

← Back to Index