Documentation Verification Report

Opposite

📁 Source: Mathlib/Algebra/Group/Equiv/Opposite.lean

Statistics

Metric	Count
Definitions `mulOp`, `mulUnop`, `neg'`, `op`, `opOp`, `unop`, `fromOpposite`, `mulOp`, `mulUnop`, `op`, `toOpposite`, `unop`, `fromOpposite`, `mulOp`, `mulUnop`, `op`, `toOpposite`, `unop`, `opAddEquiv`, `opMulEquiv`, `fromOpposite`, `op`, `toOpposite`, `unop`, `inv'`, `op`, `opOp`, `unop`, `fromOpposite`, `op`, `toOpposite`, `unop`, `opAddEquiv`, `opMulEquiv`	34
Theorems `mulOp_apply`, `mulOp_symm_apply`, `neg'_apply`, `neg'_symm_apply`, `opOp_apply`, `opOp_symm_apply`, `op_apply_apply`, `op_apply_symm_apply`, `op_symm_apply_apply`, `op_symm_apply_symm_apply`, `fromOpposite_apply`, `mulOp_apply_apply`, `mulOp_symm_apply_apply`, `op_apply_apply`, `op_symm_apply_apply`, `toOpposite_apply`, `fromOpposite_apply`, `mulOp_apply_apply`, `mulOp_symm_apply_apply`, `mul_op_ext`, `mul_op_ext_iff`, `op_apply_apply`, `op_symm_apply_apply`, `toOpposite_apply`, `coe_opAddEquiv`, `coe_symm_opAddEquiv`, `opAddEquiv_apply`, `opAddEquiv_symm_apply`, `opMulEquiv_apply`, `opMulEquiv_symm_apply`, `opMulEquiv_toEquiv`, `fromOpposite_apply`, `op_apply_apply`, `op_symm_apply_apply`, `toOpposite_apply`, `inv'_apply`, `inv'_symm_apply`, `opOp_apply`, `opOp_symm_apply`, `op_apply_apply`, `op_apply_symm_apply`, `op_symm_apply_apply`, `op_symm_apply_symm_apply`, `fromOpposite_apply`, `op_apply_apply`, `op_symm_apply_apply`, `toOpposite_apply`, `coe_opMulEquiv`, `coe_symm_opMulEquiv`, `opAddEquiv_apply`, `opAddEquiv_symm_apply`, `opAddEquiv_toEquiv`, `opMulEquiv_apply`, `opMulEquiv_symm_apply`	54
Total	88

AddEquiv

Definitions

Name	Category	Theorems
`mulOp` 📖	CompOp	2 math math: `mulOp_symm_apply`, `mulOp_apply`
`mulUnop` 📖	CompOp	—
`neg'` 📖	CompOp	2 math math: `neg'_apply`, `neg'_symm_apply`
`op` 📖	CompOp	4 math math: `op_symm_apply_symm_apply`, `op_symm_apply_apply`, `op_apply_symm_apply`, `op_apply_apply`
`opOp` 📖	CompOp	2 math math: `opOp_symm_apply`, `opOp_apply`
`unop` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mulOp_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `AddEquiv` `MulOpposite` `MulOpposite.instAdd` `EquivLike.toFunLike` `Equiv.instEquivLike` `mulOp` `trans` `symm` `MulOpposite.opAddEquiv`	—	—
`mulOp_symm_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `AddEquiv` `MulOpposite` `MulOpposite.instAdd` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `mulOp` `trans` `MulOpposite.opAddEquiv` `symm`	—	—
`neg'_apply` 📖	mathematical	—	`DFunLike.coe` `AddEquiv` `AddOpposite` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `SubtractionMonoid.toSubNegMonoid` `AddOpposite.instAdd` `EquivLike.toFunLike` `instEquivLike` `neg'` `AddOpposite.op` `InvolutiveNeg.toNeg` `SubtractionMonoid.toInvolutiveNeg`	—	—
`neg'_symm_apply` 📖	mathematical	—	`DFunLike.coe` `AddEquiv` `AddOpposite` `AddOpposite.instAdd` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `SubtractionMonoid.toSubNegMonoid` `EquivLike.toFunLike` `instEquivLike` `symm` `neg'` `InvolutiveNeg.toNeg` `SubtractionMonoid.toInvolutiveNeg` `AddOpposite.unop`	—	—
`opOp_apply` 📖	mathematical	—	`DFunLike.coe` `AddEquiv` `AddOpposite` `AddOpposite.instAdd` `EquivLike.toFunLike` `instEquivLike` `opOp` `AddOpposite.op`	—	—
`opOp_symm_apply` 📖	mathematical	—	`DFunLike.coe` `AddEquiv` `AddOpposite` `AddOpposite.instAdd` `EquivLike.toFunLike` `instEquivLike` `symm` `opOp` `AddOpposite.unop`	—	—
`op_apply_apply` 📖	mathematical	—	`DFunLike.coe` `AddEquiv` `AddOpposite` `AddOpposite.instAdd` `EquivLike.toFunLike` `instEquivLike` `Equiv` `Equiv.instEquivLike` `op` `AddOpposite.op` `AddOpposite.unop`	—	—
`op_apply_symm_apply` 📖	mathematical	—	`DFunLike.coe` `AddEquiv` `AddOpposite` `AddOpposite.instAdd` `EquivLike.toFunLike` `instEquivLike` `symm` `Equiv` `Equiv.instEquivLike` `op` `AddOpposite.op` `AddOpposite.unop`	—	—
`op_symm_apply_apply` 📖	mathematical	—	`DFunLike.coe` `AddEquiv` `EquivLike.toFunLike` `instEquivLike` `Equiv` `AddOpposite` `AddOpposite.instAdd` `Equiv.instEquivLike` `Equiv.symm` `op` `AddOpposite.unop` `AddOpposite.op`	—	—
`op_symm_apply_symm_apply` 📖	mathematical	—	`DFunLike.coe` `AddEquiv` `EquivLike.toFunLike` `instEquivLike` `symm` `Equiv` `AddOpposite` `AddOpposite.instAdd` `Equiv.instEquivLike` `Equiv.symm` `op` `AddOpposite.unop` `AddOpposite.op`	—	—

AddHom

Definitions

Name	Category	Theorems
`fromOpposite` 📖	CompOp	1 math math: `fromOpposite_apply`
`mulOp` 📖	CompOp	2 math math: `mulOp_apply_apply`, `mulOp_symm_apply_apply`
`mulUnop` 📖	CompOp	—
`op` 📖	CompOp	2 math math: `op_apply_apply`, `op_symm_apply_apply`
`toOpposite` 📖	CompOp	1 math math: `toOpposite_apply`
`unop` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`fromOpposite_apply` 📖	mathematical	`AddCommute` `DFunLike.coe` `AddHom` `funLike`	`AddOpposite` `AddOpposite.instAdd` `fromOpposite` `AddOpposite.unop`	—	—
`mulOp_apply_apply` 📖	mathematical	—	`DFunLike.coe` `AddHom` `MulOpposite` `MulOpposite.instAdd` `funLike` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `mulOp` `MulOpposite.op` `MulOpposite.unop`	—	—
`mulOp_symm_apply_apply` 📖	mathematical	—	`DFunLike.coe` `AddHom` `funLike` `Equiv` `MulOpposite` `MulOpposite.instAdd` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `mulOp` `MulOpposite.unop` `MulOpposite.op`	—	—
`op_apply_apply` 📖	mathematical	—	`DFunLike.coe` `AddHom` `AddOpposite` `AddOpposite.instAdd` `funLike` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `op` `AddOpposite.op` `AddOpposite.unop`	—	—
`op_symm_apply_apply` 📖	mathematical	—	`DFunLike.coe` `AddHom` `funLike` `Equiv` `AddOpposite` `AddOpposite.instAdd` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `op` `AddOpposite.unop` `AddOpposite.op`	—	—
`toOpposite_apply` 📖	mathematical	`AddCommute` `DFunLike.coe` `AddHom` `funLike`	`AddOpposite` `AddOpposite.instAdd` `toOpposite` `AddOpposite.op`	—	—

AddMonoidHom

Definitions

Name	Category	Theorems
`fromOpposite` 📖	CompOp	1 math math: `fromOpposite_apply`
`mulOp` 📖	CompOp	3 math math: `mulOp_apply_apply`, `NonUnitalRingHom.op_apply_apply`, `mulOp_symm_apply_apply`
`mulUnop` 📖	CompOp	1 math math: `NonUnitalRingHom.op_symm_apply_apply`
`op` 📖	CompOp	2 math math: `op_symm_apply_apply`, `op_apply_apply`
`toOpposite` 📖	CompOp	1 math math: `toOpposite_apply`
`unop` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`fromOpposite_apply` 📖	mathematical	`AddCommute` `AddZero.toAdd` `AddZeroClass.toAddZero` `DFunLike.coe` `AddMonoidHom` `instFunLike`	`AddOpposite` `AddOpposite.instAddZero` `fromOpposite` `AddOpposite.unop`	—	—
`mulOp_apply_apply` 📖	mathematical	—	`DFunLike.coe` `AddMonoidHom` `MulOpposite` `AddZeroClass.toAddZero` `MulOpposite.instAddZeroClass` `instFunLike` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `mulOp` `MulOpposite.op` `MulOpposite.unop`	—	—
`mulOp_symm_apply_apply` 📖	mathematical	—	`DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `instFunLike` `Equiv` `MulOpposite` `MulOpposite.instAddZeroClass` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `mulOp` `MulOpposite.unop` `MulOpposite.op`	—	—
`mul_op_ext` 📖	—	`comp` `MulOpposite` `AddZeroClass.toAddZero` `MulOpposite.instAddZeroClass` `AddEquiv.toAddMonoidHom` `MulOpposite.opAddEquiv` `AddZero.toAdd`	—	—	`ext` `DFunLike.congr_fun`
`mul_op_ext_iff` 📖	mathematical	—	`comp` `MulOpposite` `AddZeroClass.toAddZero` `MulOpposite.instAddZeroClass` `AddEquiv.toAddMonoidHom` `MulOpposite.opAddEquiv` `AddZero.toAdd`	—	`mul_op_ext`
`op_apply_apply` 📖	mathematical	—	`DFunLike.coe` `AddMonoidHom` `AddOpposite` `AddOpposite.instAddZero` `AddZeroClass.toAddZero` `instFunLike` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `op` `AddOpposite.op` `AddOpposite.unop`	—	—
`op_symm_apply_apply` 📖	mathematical	—	`DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `instFunLike` `Equiv` `AddOpposite` `AddOpposite.instAddZero` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `op` `AddOpposite.unop` `AddOpposite.op`	—	—
`toOpposite_apply` 📖	mathematical	`AddCommute` `AddZero.toAdd` `AddZeroClass.toAddZero` `DFunLike.coe` `AddMonoidHom` `instFunLike`	`AddOpposite` `AddOpposite.instAddZero` `toOpposite` `AddOpposite.op`	—	—

AddOpposite

Definitions

Name	Category	Theorems
`opAddEquiv` 📖	CompOp	4 math math: `opAddEquiv_apply`, `coe_opAddEquiv`, `coe_symm_opAddEquiv`, `opAddEquiv_symm_apply`
`opMulEquiv` 📖	CompOp	3 math math: `opMulEquiv_symm_apply`, `opMulEquiv_toEquiv`, `opMulEquiv_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_opAddEquiv` 📖	mathematical	—	`DFunLike.coe` `AddEquiv` `AddOpposite` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `instAdd` `EquivLike.toFunLike` `AddEquiv.instEquivLike` `opAddEquiv` `op`	—	—
`coe_symm_opAddEquiv` 📖	mathematical	—	`DFunLike.coe` `AddEquiv` `AddOpposite` `instAdd` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `EquivLike.toFunLike` `AddEquiv.instEquivLike` `AddEquiv.symm` `opAddEquiv` `unop`	—	—
`opAddEquiv_apply` 📖	mathematical	—	`DFunLike.coe` `AddEquiv` `AddOpposite` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `instAdd` `EquivLike.toFunLike` `AddEquiv.instEquivLike` `opAddEquiv` `op`	—	—
`opAddEquiv_symm_apply` 📖	mathematical	—	`DFunLike.coe` `AddEquiv` `AddOpposite` `instAdd` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `EquivLike.toFunLike` `AddEquiv.instEquivLike` `AddEquiv.symm` `opAddEquiv` `unop`	—	—
`opMulEquiv_apply` 📖	mathematical	—	`DFunLike.coe` `MulEquiv` `AddOpposite` `instMul` `EquivLike.toFunLike` `MulEquiv.instEquivLike` `opMulEquiv` `op`	—	—
`opMulEquiv_symm_apply` 📖	mathematical	—	`DFunLike.coe` `MulEquiv` `AddOpposite` `instMul` `EquivLike.toFunLike` `MulEquiv.instEquivLike` `MulEquiv.symm` `opMulEquiv` `unop`	—	—
`opMulEquiv_toEquiv` 📖	mathematical	—	`EquivLike.toEquiv` `AddOpposite` `MulEquiv` `instMul` `MulEquiv.instEquivLike` `opMulEquiv` `opEquiv`	—	—

MonoidHom

Definitions

Name	Category	Theorems
`fromOpposite` 📖	CompOp	1 math math: `fromOpposite_apply`
`op` 📖	CompOp	3 math math: `Monoid.CoprodI.inv_def`, `op_symm_apply_apply`, `op_apply_apply`
`toOpposite` 📖	CompOp	1 math math: `toOpposite_apply`
`unop` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`fromOpposite_apply` 📖	mathematical	`Commute` `MulOne.toMul` `MulOneClass.toMulOne` `DFunLike.coe` `MonoidHom` `instFunLike`	`MulOpposite` `MulOpposite.instMulOne` `fromOpposite` `MulOpposite.unop`	—	—
`op_apply_apply` 📖	mathematical	—	`DFunLike.coe` `MonoidHom` `MulOpposite` `MulOpposite.instMulOne` `MulOneClass.toMulOne` `instFunLike` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `op` `MulOpposite.op` `MulOpposite.unop`	—	—
`op_symm_apply_apply` 📖	mathematical	—	`DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `instFunLike` `Equiv` `MulOpposite` `MulOpposite.instMulOne` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `op` `MulOpposite.unop` `MulOpposite.op`	—	—
`toOpposite_apply` 📖	mathematical	`Commute` `MulOne.toMul` `MulOneClass.toMulOne` `DFunLike.coe` `MonoidHom` `instFunLike`	`MulOpposite` `MulOpposite.instMulOne` `toOpposite` `MulOpposite.op`	—	—

MulEquiv

Definitions

Name	Category	Theorems
`inv'` 📖	CompOp	3 math math: `inv'_apply`, `Monoid.CoprodI.inv_def`, `inv'_symm_apply`
`op` 📖	CompOp	4 math math: `op_apply_symm_apply`, `op_apply_apply`, `op_symm_apply_symm_apply`, `op_symm_apply_apply`
`opOp` 📖	CompOp	2 math math: `opOp_symm_apply`, `opOp_apply`
`unop` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`inv'_apply` 📖	mathematical	—	`DFunLike.coe` `MulEquiv` `MulOpposite` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `DivisionMonoid.toDivInvMonoid` `MulOpposite.instMul` `EquivLike.toFunLike` `instEquivLike` `inv'` `MulOpposite.op` `InvolutiveInv.toInv` `DivisionMonoid.toInvolutiveInv`	—	—
`inv'_symm_apply` 📖	mathematical	—	`DFunLike.coe` `MulEquiv` `MulOpposite` `MulOpposite.instMul` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `DivisionMonoid.toDivInvMonoid` `EquivLike.toFunLike` `instEquivLike` `symm` `inv'` `InvolutiveInv.toInv` `DivisionMonoid.toInvolutiveInv` `MulOpposite.unop`	—	—
`opOp_apply` 📖	mathematical	—	`DFunLike.coe` `MulEquiv` `MulOpposite` `MulOpposite.instMul` `EquivLike.toFunLike` `instEquivLike` `opOp` `MulOpposite.op`	—	—
`opOp_symm_apply` 📖	mathematical	—	`DFunLike.coe` `MulEquiv` `MulOpposite` `MulOpposite.instMul` `EquivLike.toFunLike` `instEquivLike` `symm` `opOp` `MulOpposite.unop`	—	—
`op_apply_apply` 📖	mathematical	—	`DFunLike.coe` `MulEquiv` `MulOpposite` `MulOpposite.instMul` `EquivLike.toFunLike` `instEquivLike` `Equiv` `Equiv.instEquivLike` `op` `MulOpposite.op` `MulOpposite.unop`	—	—
`op_apply_symm_apply` 📖	mathematical	—	`DFunLike.coe` `MulEquiv` `MulOpposite` `MulOpposite.instMul` `EquivLike.toFunLike` `instEquivLike` `symm` `Equiv` `Equiv.instEquivLike` `op` `MulOpposite.op` `MulOpposite.unop`	—	—
`op_symm_apply_apply` 📖	mathematical	—	`DFunLike.coe` `MulEquiv` `EquivLike.toFunLike` `instEquivLike` `Equiv` `MulOpposite` `MulOpposite.instMul` `Equiv.instEquivLike` `Equiv.symm` `op` `MulOpposite.unop` `MulOpposite.op`	—	—
`op_symm_apply_symm_apply` 📖	mathematical	—	`DFunLike.coe` `MulEquiv` `EquivLike.toFunLike` `instEquivLike` `symm` `Equiv` `MulOpposite` `MulOpposite.instMul` `Equiv.instEquivLike` `Equiv.symm` `op` `MulOpposite.unop` `MulOpposite.op`	—	—

MulHom

Definitions

Name	Category	Theorems
`fromOpposite` 📖	CompOp	1 math math: `fromOpposite_apply`
`op` 📖	CompOp	2 math math: `op_symm_apply_apply`, `op_apply_apply`
`toOpposite` 📖	CompOp	1 math math: `toOpposite_apply`
`unop` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`fromOpposite_apply` 📖	mathematical	`Commute` `DFunLike.coe` `MulHom` `funLike`	`MulOpposite` `MulOpposite.instMul` `fromOpposite` `MulOpposite.unop`	—	—
`op_apply_apply` 📖	mathematical	—	`DFunLike.coe` `MulHom` `MulOpposite` `MulOpposite.instMul` `funLike` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `op` `MulOpposite.op` `MulOpposite.unop`	—	—
`op_symm_apply_apply` 📖	mathematical	—	`DFunLike.coe` `MulHom` `funLike` `Equiv` `MulOpposite` `MulOpposite.instMul` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `op` `MulOpposite.unop` `MulOpposite.op`	—	—
`toOpposite_apply` 📖	mathematical	`Commute` `DFunLike.coe` `MulHom` `funLike`	`MulOpposite` `MulOpposite.instMul` `toOpposite` `MulOpposite.op`	—	—

MulOpposite

Definitions

Name	Category	Theorems
`opAddEquiv` 📖	CompOp	15 math math: `opAddEquiv_apply`, `coe_opLinearEquiv_symm_addEquiv`, `MonoidAlgebra.opRingEquiv_symm_apply`, `AddMonoidAlgebra.opRingEquiv_symm_apply`, `coe_opLinearEquiv_addEquiv`, `AddEquiv.mulOp_symm_apply`, `AddEquiv.mulOp_apply`, `opLinearEquiv_toAddEquiv`, `AddMonoidHom.mul_op_ext_iff`, `AddMonoidAlgebra.opRingEquiv_apply`, `opAddEquiv_toEquiv`, `Matrix.transposeAlgEquiv_symm_apply`, `opLinearEquiv_symm_toAddEquiv`, `MonoidAlgebra.opRingEquiv_apply`, `opAddEquiv_symm_apply`
`opMulEquiv` 📖	CompOp	4 math math: `coe_symm_opMulEquiv`, `opMulEquiv_apply`, `coe_opMulEquiv`, `opMulEquiv_symm_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_opMulEquiv` 📖	mathematical	—	`DFunLike.coe` `MulEquiv` `MulOpposite` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `CommMonoid.toMonoid` `instMul` `EquivLike.toFunLike` `MulEquiv.instEquivLike` `opMulEquiv` `op`	—	—
`coe_symm_opMulEquiv` 📖	mathematical	—	`DFunLike.coe` `MulEquiv` `MulOpposite` `instMul` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `CommMonoid.toMonoid` `EquivLike.toFunLike` `MulEquiv.instEquivLike` `MulEquiv.symm` `opMulEquiv` `unop`	—	—
`opAddEquiv_apply` 📖	mathematical	—	`DFunLike.coe` `AddEquiv` `MulOpposite` `instAdd` `EquivLike.toFunLike` `AddEquiv.instEquivLike` `opAddEquiv` `op`	—	—
`opAddEquiv_symm_apply` 📖	mathematical	—	`DFunLike.coe` `AddEquiv` `MulOpposite` `instAdd` `EquivLike.toFunLike` `AddEquiv.instEquivLike` `AddEquiv.symm` `opAddEquiv` `unop`	—	—
`opAddEquiv_toEquiv` 📖	mathematical	—	`EquivLike.toEquiv` `MulOpposite` `AddEquiv` `instAdd` `AddEquiv.instEquivLike` `opAddEquiv` `opEquiv`	—	—
`opMulEquiv_apply` 📖	mathematical	—	`DFunLike.coe` `MulEquiv` `MulOpposite` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `CommMonoid.toMonoid` `instMul` `EquivLike.toFunLike` `MulEquiv.instEquivLike` `opMulEquiv` `op`	—	—
`opMulEquiv_symm_apply` 📖	mathematical	—	`DFunLike.coe` `MulEquiv` `MulOpposite` `instMul` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `CommMonoid.toMonoid` `EquivLike.toFunLike` `MulEquiv.instEquivLike` `MulEquiv.symm` `opMulEquiv` `unop`	—	—

---

← Back to Index