Opposite

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

Statistics

Metric	Count
Definitions instDistribMulAction, instMulActionWithZero, instMulDistribMulAction, instSMulWithZero, instSMulZeroClass	5
Theorems toFaithfulSMul_opposite	1
Total	6

IsLeftCancelMulZero

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
toFaithfulSMul_opposite 📖	mathematical	—	FaithfulSMul MulOpposite SMulZeroClass.toSMul MulZeroClass.toZero MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass SMulWithZero.toSMulZeroClass MulOpposite.instZero MulZeroClass.toOppositeSMulWithZero	—	subsingleton_or_nontrivial MulOpposite.instSubsingleton MulOpposite.unop_injective mul_left_cancel₀ one_ne_zero NeZero.one

MulOpposite

Definitions

Name	Category	Theorems
instDistribMulAction 📖	CompOp	2 math math: CStarMatrix.norm_def', CStarMatrix.toCLMNonUnitalAlgHom_eq_toCLM
instMulActionWithZero 📖	CompOp	—
instMulDistribMulAction 📖	CompOp	—
instSMulWithZero 📖	CompOp	—
instSMulZeroClass 📖	CompOp	—

---

← Back to Index