Documentation Verification Report

End

📁 Source: Mathlib/Algebra/Group/Action/End.lean

Statistics

Metric	Count
Definitions `ofEndHom`, `toEndHom`, `toPermHom`, `applyMulAction`, `applyMulAction`, `applyAddAction`, `applyMulAction`, `ofEndHom`, `toEndHom`, `toPermHom`, `applyMulAction`, `applyMulDistribMulAction`, `toMulAut`, `toMulEquiv`, `mulAutArrow`	15
Theorems `coe_toPermHom`, `toPermHom_apply_apply`, `toPermHom_apply_symm_apply`, `toPerm_zero`, `apply_faithfulSMul`, `smul_def`, `applyFaithfulSMul`, `instIsPretransitive`, `smul_def`, `apply_FaithfulSMul`, `mul_def`, `one_def`, `smul_def`, `coe_toPermHom`, `toPermHom_apply`, `toPerm_one`, `apply_faithfulSMul`, `smul_def`, `toMulAut_apply`, `toMulEquiv_apply`, `toMulEquiv_symm_apply`, `mulAutArrow_apply_apply`, `mulAutArrow_apply_symm_apply`	23
Total	38

AddAction

Definitions

Name	Category	Theorems
`ofEndHom` 📖	CompOp	—
`toEndHom` 📖	CompOp	—
`toPermHom` 📖	CompOp	3 math math: `toPermHom_apply_symm_apply`, `toPermHom_apply_apply`, `coe_toPermHom`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_toPermHom` 📖	mathematical	—	`DFunLike.coe` `AddMonoidHom` `Additive` `Equiv.Perm` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `Additive.addZeroClass` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Equiv.Perm.permGroup` `AddMonoidHom.instFunLike` `toPermHom` `toPerm`	—	—
`toPermHom_apply_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `AddMonoidHom` `Additive` `Equiv.Perm` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `Additive.addZeroClass` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Equiv.Perm.permGroup` `AddMonoidHom.instFunLike` `toPermHom` `HVAdd.hVAdd` `instHVAdd` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `toAddSemigroupAction`	—	—
`toPermHom_apply_symm_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `AddMonoidHom` `Additive` `Equiv.Perm` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `Additive.addZeroClass` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Equiv.Perm.permGroup` `AddMonoidHom.instFunLike` `toPermHom` `Multiplicative` `SemigroupAction.toSMul` `Monoid.toSemigroup` `Multiplicative.group` `MulAction.toSemigroupAction` `Multiplicative.mulAction` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `Multiplicative.ofAdd`	—	—
`toPerm_zero` 📖	mathematical	—	`toPerm` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `Equiv.Perm` `Equiv.Perm.instOne`	—	`Equiv.Perm.ext` `zero_vadd`

AddAut

Definitions

Name	Category	Theorems
`applyMulAction` 📖	CompOp	2 math math: `apply_faithfulSMul`, `smul_def`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`apply_faithfulSMul` 📖	mathematical	—	`FaithfulSMul` `AddAut` `AddSemigroup.toAdd` `AddMonoid.toAddSemigroup` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `instGroup` `MulAction.toSemigroupAction` `applyMulAction`	—	`AddEquiv.ext`
`smul_def` 📖	mathematical	—	`AddAut` `AddSemigroup.toAdd` `AddMonoid.toAddSemigroup` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `instGroup` `MulAction.toSemigroupAction` `applyMulAction` `DFunLike.coe` `AddEquiv` `EquivLike.toFunLike` `AddEquiv.instEquivLike`	—	—

Equiv.Perm

Definitions

Name	Category	Theorems
`applyMulAction` 📖	CompOp	40 math math: `smul_def`, `alternatingGroup.isPreprimitive_of_three_le_card`, `Set.powersetCard.isPretransitive`, `exists_mem_stabilizer_smul_eq`, `DomMulAct.mem_stabilizer_iff`, `exists_mem_stabilizer_isThreeCycle_of_two_lt_ncard`, `AlternatingGroup.isPreprimitive_of_three_le_card`, `alternatingGroup.isCoatom_stabilizer_singleton`, `mem_closure_isSwap`, `Set.powersetCard.isPretransitive_alternatingGroup`, `alternatingGroup.stabilizer.surjective_toPerm`, `finite_compl_fixedBy_swap`, `swap_mem_stabilizer`, `IsSwap.finite_compl_fixedBy`, `stabilizer_isPreprimitive`, `applyFaithfulSMul`, `swap_mem_closure_isSwap`, `Equiv.swap_mem_stabilizer`, `AlternatingGroup.isMultiplyPretransitive`, `alternatingGroup.exists_mem_stabilizer_smul_eq`, `isPretransitive_of_isCycle_mem`, `exists_mem_stabilizer_isThreeCycle`, `instIsPreprimitive`, `AlternatingGroup.isPretransitive_of_three_le_card`, `alternatingGroup.stabilizer_isPreprimitive`, `mem_closure_isSwap'`, `DomMulAct.stabilizerMulEquiv_apply`, `alternatingGroup.isCoatom_stabilizer`, `Set.powersetCard.isPreprimitive_perm`, `isCoatom_stabilizer`, `Set.powersetCard.isPreprimitive_alternatingGroup`, `alternatingGroup.isPretransitive_of_three_le_card`, `instIsPretransitive`, `alternatingGroup.isMultiplyPretransitive`, `stabilizer.surjective_toPerm`, `isCoatom_stabilizer_of_ncard_lt_ncard_compl`, `moves_in`, `ofSubtype_mem_stabilizer`, `alternatingGroup.isCoatom_stabilizer_of_ncard_lt_ncard_compl`, `isMultiplyPretransitive`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`applyFaithfulSMul` 📖	mathematical	—	`FaithfulSMul` `Equiv.Perm` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `permGroup` `MulAction.toSemigroupAction` `applyMulAction`	—	`Equiv.ext`
`instIsPretransitive` 📖	mathematical	—	`MulAction.IsPretransitive` `Equiv.Perm` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `permGroup` `MulAction.toSemigroupAction` `applyMulAction`	—	`MulAction.isPretransitive_iff` `Equiv.swap_apply_left`
`smul_def` 📖	mathematical	—	`Equiv.Perm` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `permGroup` `MulAction.toSemigroupAction` `applyMulAction` `DFunLike.coe` `EquivLike.toFunLike` `Equiv.instEquivLike`	—	—

Function.End

Definitions

Name	Category	Theorems
`applyAddAction` 📖	CompOp	—
`applyMulAction` 📖	CompOp	2 math math: `smul_def`, `apply_FaithfulSMul`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`apply_FaithfulSMul` 📖	mathematical	—	`FaithfulSMul` `Function.End` `SemigroupAction.toSMul` `Monoid.toSemigroup` `instMonoidEnd` `MulAction.toSemigroupAction` `applyMulAction`	—	—
`mul_def` 📖	mathematical	—	`Function.End` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `instMonoidEnd`	—	—
`one_def` 📖	mathematical	—	`Function.End` `MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `instMonoidEnd`	—	—
`smul_def` 📖	mathematical	—	`Function.End` `SemigroupAction.toSMul` `Monoid.toSemigroup` `instMonoidEnd` `MulAction.toSemigroupAction` `applyMulAction`	—	—

MulAction

Definitions

Name	Category	Theorems
`ofEndHom` 📖	CompOp	—
`toEndHom` 📖	CompOp	1 math math: `Action.ofMulAction_ρ`
`toPermHom` 📖	CompOp	5 math math: `toPermHom_apply`, `Subgroup.normalCore_eq_ker`, `Polynomial.Splits.toPermHom_apply_eq_one_or_isSwap_of_ncard_le_of_mem_inertia`, `Polynomial.Splits.surjective_toPermHom_of_iSup_inertia_eq_top`, `coe_toPermHom`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_toPermHom` 📖	mathematical	—	`DFunLike.coe` `MonoidHom` `Equiv.Perm` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Equiv.Perm.permGroup` `MonoidHom.instFunLike` `toPermHom` `toPerm`	—	—
`toPermHom_apply` 📖	mathematical	—	`DFunLike.coe` `MonoidHom` `Equiv.Perm` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Equiv.Perm.permGroup` `MonoidHom.instFunLike` `toPermHom` `toPerm`	—	—
`toPerm_one` 📖	mathematical	—	`toPerm` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `Equiv.Perm` `Equiv.Perm.instOne`	—	`Equiv.Perm.ext` `one_smul`

MulAut

Definitions

Name	Category	Theorems
`applyMulAction` 📖	CompOp	3 math math: `Sylow.coe_smul`, `smul_def`, `apply_faithfulSMul`
`applyMulDistribMulAction` 📖	CompOp	8 math math: `Subgroup.conj_smul_subgroupOf`, `Subgroup.Normal.conj_smul_eq_self`, `Subgroup.conj_smul_le_of_le`, `Sylow.coe_subgroup_smul`, `IsGalois.map_fixingSubgroup`, `Subgroup.conj_smul_eq_self_of_mem`, `MulAction.IwasawaStructure.is_conj`, `Sylow.smul_def`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`apply_faithfulSMul` 📖	mathematical	—	`FaithfulSMul` `MulAut` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `instGroup` `MulAction.toSemigroupAction` `applyMulAction`	—	`MulEquiv.ext`
`smul_def` 📖	mathematical	—	`MulAut` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `instGroup` `MulAction.toSemigroupAction` `applyMulAction` `DFunLike.coe` `MulEquiv` `EquivLike.toFunLike` `MulEquiv.instEquivLike`	—	—

MulDistribMulAction

Definitions

Name	Category	Theorems
`toMulAut` 📖	CompOp	1 math math: `toMulAut_apply`
`toMulEquiv` 📖	CompOp	5 math math: `Subgroup.equivSMul_apply_coe`, `toMulEquiv_apply`, `toMulEquiv_symm_apply`, `toMulAut_apply`, `Subgroup.equivSMul_symm_apply_coe`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`toMulAut_apply` 📖	mathematical	—	`DFunLike.coe` `MonoidHom` `MulAut` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAut.instGroup` `MonoidHom.instFunLike` `toMulAut` `toMulEquiv`	—	—
`toMulEquiv_apply` 📖	mathematical	—	`DFunLike.coe` `MulEquiv` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `EquivLike.toFunLike` `MulEquiv.instEquivLike` `toMulEquiv` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction` `toMulAction`	—	—
`toMulEquiv_symm_apply` 📖	mathematical	—	`DFunLike.coe` `MulEquiv` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `EquivLike.toFunLike` `MulEquiv.instEquivLike` `MulEquiv.symm` `toMulEquiv` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction` `toMulAction` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	—	—

(root)

Definitions

Name	Category	Theorems
`mulAutArrow` 📖	CompOp	4 math math: `mulAutArrow_apply_apply`, `mulAutArrow_apply_symm_apply`, `CategoryTheory.ActionCategory.curry_apply_left`, `CategoryTheory.ActionCategory.curry_apply_right`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mulAutArrow_apply_apply` 📖	mathematical	—	`DFunLike.coe` `MulEquiv` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `Pi.monoid` `EquivLike.toFunLike` `MulEquiv.instEquivLike` `MonoidHom` `MulAut` `Pi.instMul` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAut.instGroup` `MonoidHom.instFunLike` `mulAutArrow` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MulAction.toSemigroupAction` `MulDistribMulAction.toMulAction` `arrowMulDistribMulAction` `Group.toDivisionMonoid`	—	—
`mulAutArrow_apply_symm_apply` 📖	mathematical	—	`DFunLike.coe` `MulEquiv` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `Pi.monoid` `EquivLike.toFunLike` `MulEquiv.instEquivLike` `MulEquiv.symm` `MonoidHom` `MulAut` `Pi.instMul` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAut.instGroup` `MonoidHom.instFunLike` `mulAutArrow` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MulAction.toSemigroupAction` `MulDistribMulAction.toMulAction` `arrowMulDistribMulAction` `Group.toDivisionMonoid` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid`	—	—

---

← Back to Index