Basic

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

Statistics

Metric	Count
Definitions applyDistribMulAction, toAddAut, toAddEquiv, smulMonoidWithZeroHom	4
Theorems toAddAut_apply, toAddEquiv_apply, toAddEquiv_symm_apply, smul_sub_iff_sub_inv_smul, bijective₀, injective₀, surjective₀, smulMonoidWithZeroHom_apply, smul_zpow₀'	9
Total	13

AddAut

Definitions

Name	Category	Theorems
applyDistribMulAction 📖	CompOp	—

DistribMulAction

Definitions

Name	Category	Theorems
toAddAut 📖	CompOp	1 math math: toAddAut_apply
toAddEquiv 📖	CompOp	3 math math: toAddEquiv_apply, toAddEquiv_symm_apply, toAddAut_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
toAddAut_apply 📖	mathematical	—	DFunLike.coe MonoidHom AddAut AddSemigroup.toAdd AddMonoid.toAddSemigroup MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid AddAut.instGroup MonoidHom.instFunLike toAddAut toAddEquiv	—	—
toAddEquiv_apply 📖	mathematical	—	DFunLike.coe AddEquiv AddSemigroup.toAdd AddMonoid.toAddSemigroup EquivLike.toFunLike AddEquiv.instEquivLike toAddEquiv SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass DistribSMul.toSMulZeroClass toDistribSMul DivInvMonoid.toMonoid Group.toDivInvMonoid	—	—
toAddEquiv_symm_apply 📖	mathematical	—	DFunLike.coe AddEquiv AddSemigroup.toAdd AddMonoid.toAddSemigroup EquivLike.toFunLike AddEquiv.instEquivLike AddEquiv.symm toAddEquiv SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid MulAction.toSemigroupAction toMulAction InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	—	—

IsUnit

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
smul_sub_iff_sub_inv_smul 📖	mathematical	—	IsUnit SubNegMonoid.toSub AddGroup.toSubNegMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul DivInvMonoid.toMonoid Group.toDivInvMonoid MulOne.toOne MulOneClass.toMulOne Monoid.toMulOneClass InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	—	isUnit_smul_iff smul_sub smul_inv_smul

MulAction

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
bijective₀ 📖	mathematical	—	Function.Bijective SemigroupAction.toSMul Monoid.toSemigroup MonoidWithZero.toMonoid GroupWithZero.toMonoidWithZero toSemigroupAction	—	bijective
injective₀ 📖	mathematical	—	SemigroupAction.toSMul Monoid.toSemigroup MonoidWithZero.toMonoid GroupWithZero.toMonoidWithZero toSemigroupAction	—	Function.Bijective.injective bijective₀
surjective₀ 📖	mathematical	—	SemigroupAction.toSMul Monoid.toSemigroup MonoidWithZero.toMonoid GroupWithZero.toMonoidWithZero toSemigroupAction	—	Function.Bijective.surjective bijective₀

(root)

Definitions

Name	Category	Theorems
smulMonoidWithZeroHom 📖	CompOp	1 math math: smulMonoidWithZeroHom_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
smulMonoidWithZeroHom_apply 📖	mathematical	—	DFunLike.coe MonoidWithZeroHom Prod.instMulZeroOneClass MonoidWithZero.toMulZeroOneClass MonoidWithZeroHom.funLike smulMonoidWithZeroHom OneHom.toFun MulOne.toOne MulOneClass.toMulOne Prod.instMulOneClass Monoid.toMulOneClass MonoidWithZero.toMonoid MulZeroOneClass.toMulOneClass MonoidHom.toOneHom smulMonoidHom MulActionWithZero.toMulAction MulZeroClass.toZero MulZeroOneClass.toMulZeroClass	—	—
smul_zpow₀' 📖	mathematical	—	SMulZeroClass.toSMul MulZeroClass.toZero MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass GroupWithZero.toMonoidWithZero instSMulZeroClass DivInvMonoid.toZPow GroupWithZero.toDivInvMonoid	—	zpow_natCast smul_pow' zpow_negSucc smul_inv₀'

---

← Back to Index