ConjAct

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

Statistics

Metric	Count
Definitions instGroupWithZero, mulAction₀	2
Theorems ofConjAct_zero, smulCommClass₀, smulCommClass₀', toConjAct_zero	4
Total	6

ConjAct

Definitions

Name	Category	Theorems
instGroupWithZero 📖	CompOp	2 math math: toConjAct_zero, ofConjAct_zero
mulAction₀ 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ofConjAct_zero 📖	mathematical	—	DFunLike.coe MulEquiv ConjAct MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid instDivInvMonoid GroupWithZero.toDivInvMonoid EquivLike.toFunLike MulEquiv.instEquivLike ofConjAct MulZeroClass.toZero MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass GroupWithZero.toMonoidWithZero instGroupWithZero	—	—
smulCommClass₀ 📖	mathematical	—	SMulCommClass ConjAct instSMul GroupWithZero.toDivInvMonoid	—	smul_def mul_smul_comm smul_mul_assoc
smulCommClass₀' 📖	mathematical	—	SMulCommClass ConjAct instSMul GroupWithZero.toDivInvMonoid	—	SMulCommClass.symm smulCommClass₀
toConjAct_zero 📖	mathematical	—	DFunLike.coe MulEquiv ConjAct MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid GroupWithZero.toDivInvMonoid instDivInvMonoid EquivLike.toFunLike MulEquiv.instEquivLike toConjAct MulZeroClass.toZero MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass GroupWithZero.toMonoidWithZero instGroupWithZero	—	—

---

← Back to Index