Documentation Verification Report

Basic

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

Statistics

Metric	Count
Definitions `toFun`, `toPerm`, `mulDistribMulAction`, `mulDistribMulAction`, `toFun`, `toPerm`, `toMonoidEnd`, `toMonoidHom`, `arrowAction`, `arrowAddAction`, `arrowMulDistribMulAction`	11
Theorems `bijective`, `injective`, `surjective`, `toFun_apply`, `toPerm_apply`, `toPerm_injective`, `toPerm_symm_apply`, `vadd_bijective`, `vadd_left_cancel`, `smul_bijective`, `smul_left_cancel`, `bijective`, `injective`, `surjective`, `toFun_apply`, `toPerm_apply`, `toPerm_injective`, `toPerm_symm_apply`, `toMonoidEnd_apply`, `toMonoidHom_apply`, `arrowAction_smul`, `arrowAddAction_vadd`, `invOf_smul_eq_iff`, `invOf_smul_smul`, `isCancelSMul_iff_eq_one_of_smul_eq`, `isCancelVAdd_iff_eq_zero_of_vadd_eq`, `isUnit_smul_iff`, `smul_div'`, `smul_eq_iff_eq_invOf_smul`, `smul_eq_iff_eq_inv_smul`, `smul_inv'`, `smul_invOf_smul`, `smul_left_cancel`, `smul_left_cancel_iff`, `smul_pow'`, `smul_zpow'`, `vadd_eq_iff_eq_neg_vadd`, `vadd_left_cancel`, `vadd_left_cancel_iff`	39
Total	50

AddAction

Definitions

Name	Category	Theorems
`toFun` 📖	CompOp	1 math math: `toFun_apply`
`toPerm` 📖	CompOp	9 math math: `IsometryEquiv.constVAdd_toEquiv`, `toPerm_zero`, `toPerm_injective`, `toPerm_symm_apply`, `Set.powersetCard.addAction_faithful`, `coe_toPermHom`, `MeasurableEquiv.vadd_toEquiv`, `toPerm_apply`, `Function.Embedding.vadd_def`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`bijective` 📖	mathematical	—	`Function.Bijective` `HVAdd.hVAdd` `instHVAdd` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `toAddSemigroupAction`	—	`Equiv.bijective`
`injective` 📖	mathematical	—	`HVAdd.hVAdd` `instHVAdd` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `toAddSemigroupAction`	—	`Function.Bijective.injective` `bijective`
`surjective` 📖	mathematical	—	`HVAdd.hVAdd` `instHVAdd` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `toAddSemigroupAction`	—	`Function.Bijective.surjective` `bijective`
`toFun_apply` 📖	mathematical	—	`DFunLike.coe` `Function.Embedding` `Function.instFunLikeEmbedding` `toFun` `HVAdd.hVAdd` `instHVAdd` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `toAddSemigroupAction`	—	—
`toPerm_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `toPerm` `HVAdd.hVAdd` `instHVAdd` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `toAddSemigroupAction`	—	—
`toPerm_injective` 📖	mathematical	—	`Equiv.Perm` `toPerm`	—	`Function.Injective.of_comp` `vadd_left_injective'`
`toPerm_symm_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `toPerm` `HVAdd.hVAdd` `instHVAdd` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `toAddSemigroupAction` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid`	—	—

Function.Injective

Definitions

Name	Category	Theorems
`mulDistribMulAction` 📖	CompOp	—

Function.Surjective

Definitions

Name	Category	Theorems
`mulDistribMulAction` 📖	CompOp	—

IsAddUnit

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`vadd_bijective` 📖	mathematical	`IsAddUnit`	`Function.Bijective` `HVAdd.hVAdd` `instHVAdd` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `AddAction.toAddSemigroupAction`	—	`CanLift.prf` `instCanLiftAddUnitsValIsAddUnit` `AddAction.bijective`
`vadd_left_cancel` 📖	mathematical	`IsAddUnit`	`HVAdd.hVAdd` `instHVAdd` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `AddAction.toAddSemigroupAction`	—	`vadd_left_cancel_iff`

IsUnit

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`smul_bijective` 📖	mathematical	`IsUnit`	`Function.Bijective` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MulAction.toSemigroupAction`	—	`CanLift.prf` `instCanLiftUnitsValIsUnit` `MulAction.bijective`
`smul_left_cancel` 📖	mathematical	`IsUnit`	`SemigroupAction.toSMul` `Monoid.toSemigroup` `MulAction.toSemigroupAction`	—	`smul_left_cancel_iff`

MulAction

Definitions

Name	Category	Theorems
`toFun` 📖	CompOp	2 math math: `toFun_apply`, `FixedPoints.linearIndependent_smul_of_linearIndependent`
`toPerm` 📖	CompOp	12 math math: `MeasurableEquiv.smul_toEquiv`, `toPerm_apply`, `IsometryEquiv.constSMul_toEquiv`, `alternatingGroup.stabilizer.surjective_toPerm`, `toPerm_symm_apply`, `toPermHom_apply`, `Function.Embedding.smul_def`, `toPerm_injective`, `Set.powersetCard.mulAction_faithful`, `Equiv.Perm.stabilizer.surjective_toPerm`, `coe_toPermHom`, `toPerm_one`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`bijective` 📖	mathematical	—	`Function.Bijective` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `toSemigroupAction`	—	`Equiv.bijective`
`injective` 📖	mathematical	—	`SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `toSemigroupAction`	—	`Function.Bijective.injective` `bijective`
`surjective` 📖	mathematical	—	`SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `toSemigroupAction`	—	`Function.Bijective.surjective` `bijective`
`toFun_apply` 📖	mathematical	—	`DFunLike.coe` `Function.Embedding` `Function.instFunLikeEmbedding` `toFun` `SemigroupAction.toSMul` `Monoid.toSemigroup` `toSemigroupAction`	—	—
`toPerm_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `toPerm` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `toSemigroupAction`	—	—
`toPerm_injective` 📖	mathematical	—	`Equiv.Perm` `toPerm`	—	`Function.Injective.of_comp` `smul_left_injective'`
`toPerm_symm_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `toPerm` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `toSemigroupAction` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	—	—

MulDistribMulAction

Definitions

Name	Category	Theorems
`toMonoidEnd` 📖	CompOp	2 math math: `Subgroup.pointwise_smul_def`, `toMonoidEnd_apply`
`toMonoidHom` 📖	CompOp	2 math math: `toMonoidHom_apply`, `toMonoidEnd_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`toMonoidEnd_apply` 📖	mathematical	—	`DFunLike.coe` `MonoidHom` `Monoid.End` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `Monoid.End.instMonoid` `MonoidHom.instFunLike` `toMonoidEnd` `toMonoidHom`	—	—
`toMonoidHom_apply` 📖	mathematical	—	`DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `MonoidHom.instFunLike` `toMonoidHom` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MulAction.toSemigroupAction` `toMulAction`	—	—

(root)

Definitions

Name	Category	Theorems
`arrowAction` 📖	CompOp	1 math math: `arrowAction_smul`
`arrowAddAction` 📖	CompOp	1 math math: `arrowAddAction_vadd`
`arrowMulDistribMulAction` 📖	CompOp	2 math math: `mulAutArrow_apply_apply`, `mulAutArrow_apply_symm_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`arrowAction_smul` 📖	mathematical	—	`SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `DivisionMonoid.toDivInvMonoid` `MulAction.toSemigroupAction` `arrowAction` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid`	—	—
`arrowAddAction_vadd` 📖	mathematical	—	`VAdd.vadd` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `SubtractionMonoid.toSubNegMonoid` `AddAction.toAddSemigroupAction` `arrowAddAction` `HVAdd.hVAdd` `instHVAdd` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid`	—	—
`invOf_smul_eq_iff` 📖	mathematical	—	`SemigroupAction.toSMul` `Monoid.toSemigroup` `MulAction.toSemigroupAction` `Invertible.invOf` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `MulOne.toOne`	—	`inv_smul_eq_iff`
`invOf_smul_smul` 📖	mathematical	—	`SemigroupAction.toSMul` `Monoid.toSemigroup` `MulAction.toSemigroupAction` `Invertible.invOf` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `MulOne.toOne`	—	`inv_smul_smul`
`isCancelSMul_iff_eq_one_of_smul_eq` 📖	mathematical	—	`IsCancelSMul` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	—	`IsCancelSMul.eq_one_of_smul` `instIsLeftCancelSMul_1` `smul_eq_iff_eq_inv_smul` `SemigroupAction.mul_smul` `inv_mul_eq_one`
`isCancelVAdd_iff_eq_zero_of_vadd_eq` 📖	mathematical	—	`IsCancelVAdd` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.toAddSemigroupAction` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid`	—	`IsCancelVAdd.eq_zero_of_vadd` `instIsLeftCancelVAdd_1` `vadd_eq_iff_eq_neg_vadd` `AddSemigroupAction.add_vadd` `neg_add_eq_zero`
`isUnit_smul_iff` 📖	mathematical	—	`IsUnit` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction`	—	`IsUnit.smul` `inv_smul_smul`
`smul_div'` 📖	mathematical	—	`SemigroupAction.toSMul` `Monoid.toSemigroup` `MulAction.toSemigroupAction` `MulDistribMulAction.toMulAction` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `DivInvMonoid.toDiv`	—	`map_div` `MonoidHom.instMonoidHomClass`
`smul_eq_iff_eq_invOf_smul` 📖	mathematical	—	`SemigroupAction.toSMul` `Monoid.toSemigroup` `MulAction.toSemigroupAction` `Invertible.invOf` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `MulOne.toOne`	—	`smul_eq_iff_eq_inv_smul`
`smul_eq_iff_eq_inv_smul` 📖	mathematical	—	`SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	—	`Equiv.apply_eq_iff_eq_symm_apply`
`smul_inv'` 📖	mathematical	—	`SemigroupAction.toSMul` `Monoid.toSemigroup` `MulAction.toSemigroupAction` `MulDistribMulAction.toMulAction` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	—	`MonoidHom.map_inv`
`smul_invOf_smul` 📖	mathematical	—	`SemigroupAction.toSMul` `Monoid.toSemigroup` `MulAction.toSemigroupAction` `Invertible.invOf` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `MulOne.toOne`	—	`smul_inv_smul`
`smul_left_cancel` 📖	—	`SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction`	—	—	`MulAction.injective`
`smul_left_cancel_iff` 📖	mathematical	—	`SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction`	—	`MulAction.injective`
`smul_pow'` 📖	mathematical	—	`SemigroupAction.toSMul` `Monoid.toSemigroup` `MulAction.toSemigroupAction` `MulDistribMulAction.toMulAction` `Monoid.toNatPow`	—	`MonoidHom.map_pow`
`smul_zpow'` 📖	mathematical	—	`SemigroupAction.toSMul` `Monoid.toSemigroup` `MulAction.toSemigroupAction` `MulDistribMulAction.toMulAction` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `DivInvMonoid.toZPow`	—	`map_zpow` `MonoidHom.instMonoidHomClass`
`vadd_eq_iff_eq_neg_vadd` 📖	mathematical	—	`HVAdd.hVAdd` `instHVAdd` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.toAddSemigroupAction` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid`	—	`Equiv.apply_eq_iff_eq_symm_apply`
`vadd_left_cancel` 📖	—	`HVAdd.hVAdd` `instHVAdd` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.toAddSemigroupAction`	—	—	`AddAction.injective`
`vadd_left_cancel_iff` 📖	mathematical	—	`HVAdd.hVAdd` `instHVAdd` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.toAddSemigroupAction`	—	`AddAction.injective`

---

← Back to Index