Basic

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

Statistics

Metric	Count
Definitions	0
Theorems image_inv, preimage_inv, swap_smul_involutive, swap_smul_self_smul, perm_inv, perm_pow, perm_zpow, perm_pow, perm_pow	9
Total	9

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

Equiv.Perm

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
image_inv 📖	mathematical	—	Set.image DFunLike.coe Equiv.Perm EquivLike.toFunLike Equiv.instEquivLike instInv Set.preimage	—	Equiv.image_symm_eq_preimage
preimage_inv 📖	mathematical	—	Set.preimage DFunLike.coe Equiv.Perm EquivLike.toFunLike Equiv.instEquivLike instInv Set.image	—	Equiv.image_eq_preimage_symm

Set.BijOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
perm_inv 📖	mathematical	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	Equiv.Perm.instPowNat	—	iterate
perm_zpow 📖	mathematical	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	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	Equiv.Perm.instPowNat	—	iterate

---

← Back to Index