Opposite

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

Statistics

Metric	Count
Definitions `moduleEndSelf`, `moduleEndSelfOp`, `op`, `opComm`, `opOp`, `toOpposite`, `unop`, `fromOpposite`, `op`, `opComm`, `toOpposite`, `unop`, `instAlgebra`	13
Theorems `moduleEndSelfOp_apply_apply`, `moduleEndSelfOp_symm_apply`, `moduleEndSelf_apply_apply`, `moduleEndSelf_symm_apply`, `opComm_apply_apply`, `opComm_apply_symm_apply`, `opComm_symm_apply_apply`, `opComm_symm_apply_symm_apply`, `opOp_apply`, `opOp_symm_apply`, `op_apply_apply`, `op_apply_symm_apply`, `op_symm_apply_apply`, `op_symm_apply_symm_apply`, `toAlgHom_op`, `toAlgHom_unop`, `toLinearEquiv_toOpposite`, `toOpposite_apply`, `toOpposite_symm_apply`, `toRingEquiv_op`, `toRingEquiv_opOp`, `toRingEquiv_toOpposite`, `toRingEquiv_unop`, `fromOpposite_apply`, `opComm_apply_apply`, `opComm_symm_apply_apply`, `op_apply_apply`, `op_symm_apply_apply`, `toLinearMap_fromOpposite`, `toLinearMap_toOpposite`, `toOpposite_apply`, `toRingHom_fromOpposite`, `toRingHom_op`, `toRingHom_toOpposite`, `toRingHom_unop`, `algebraMap_apply`	36
Total	49

AlgEquiv

Definitions

Name	Category	Theorems
`moduleEndSelf` 📖	CompOp	2 math math: `moduleEndSelf_apply_apply`, `moduleEndSelf_symm_apply`
`moduleEndSelfOp` 📖	CompOp	2 math math: `moduleEndSelfOp_apply_apply`, `moduleEndSelfOp_symm_apply`
`op` 📖	CompOp	8 math math: `op_apply_apply`, `toAlgHom_op`, `op_apply_symm_apply`, `IsAzumaya.mulLeftRight_comp_congr`, `op_symm_apply_symm_apply`, `opComm_apply_symm_apply`, `toRingEquiv_op`, `op_symm_apply_apply`
`opComm` 📖	CompOp	5 math math: `opComm_apply_apply`, `CliffordAlgebra.reverseOpEquiv_opComm`, `opComm_apply_symm_apply`, `opComm_symm_apply_apply`, `opComm_symm_apply_symm_apply`
`opOp` 📖	CompOp	5 math math: `opOp_apply`, `toRingEquiv_opOp`, `opComm_apply_symm_apply`, `opComm_symm_apply_symm_apply`, `opOp_symm_apply`
`toOpposite` 📖	CompOp	5 math math: `toOpposite_apply`, `toOpposite_symm_apply`, `toLinearEquiv_toOpposite`, `CliffordAlgebra.toBaseChange_comp_reverseOp`, `toRingEquiv_toOpposite`
`unop` 📖	CompOp	2 math math: `toRingEquiv_unop`, `toAlgHom_unop`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`moduleEndSelfOp_apply_apply` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `MulOpposite` `MulOpposite.instSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toOppositeModule` `LinearMap.instFunLike` `AlgEquiv` `Module.End` `Module.End.instSemiring` `Module.End.instAlgebra` `Algebra.toModule` `IsScalarTower.to_smulCommClass'` `MulOpposite.instAlgebra` `IsScalarTower.opposite_mid` `MulZeroClass.toMul` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `Semiring.toMonoidWithZero` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `CommSemiring.toSemiring` `Module.toDistribMulAction` `Algebra.to_smulCommClass` `MulOpposite.instSMul` `Algebra.toSMul` `instFunLike` `moduleEndSelfOp` `NonUnitalNonAssocSemiring.toMulZeroClass`	—	`IsScalarTower.to_smulCommClass'` `IsScalarTower.opposite_mid` `Algebra.to_smulCommClass`
`moduleEndSelfOp_symm_apply` 📖	mathematical	—	`DFunLike.coe` `AlgEquiv` `Module.End` `MulOpposite` `MulOpposite.instSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toOppositeModule` `Module.End.instSemiring` `Module.End.instAlgebra` `Algebra.toModule` `IsScalarTower.to_smulCommClass'` `MulOpposite.instAlgebra` `IsScalarTower.opposite_mid` `MulZeroClass.toMul` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `Semiring.toMonoidWithZero` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `CommSemiring.toSemiring` `Module.toDistribMulAction` `Algebra.to_smulCommClass` `MulOpposite.instSMul` `Algebra.toSMul` `instFunLike` `symm` `moduleEndSelfOp` `LinearMap.instFunLike` `RingHom.id` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	—	`IsScalarTower.to_smulCommClass'` `IsScalarTower.opposite_mid` `Algebra.to_smulCommClass`
`moduleEndSelf_apply_apply` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule` `LinearMap.instFunLike` `AlgEquiv` `MulOpposite` `Module.End` `MulOpposite.instSemiring` `Module.End.instSemiring` `MulOpposite.instAlgebra` `Module.End.instAlgebra` `Algebra.toModule` `IsScalarTower.to_smulCommClass'` `IsScalarTower.right` `Algebra.toSMul` `instFunLike` `moduleEndSelf` `MulZeroClass.toMul` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `Semiring.toMonoidWithZero` `MulOpposite.unop`	—	`IsScalarTower.to_smulCommClass'` `IsScalarTower.right`
`moduleEndSelf_symm_apply` 📖	mathematical	—	`DFunLike.coe` `AlgEquiv` `Module.End` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `MulOpposite` `Module.End.instSemiring` `MulOpposite.instSemiring` `Module.End.instAlgebra` `Algebra.toModule` `IsScalarTower.to_smulCommClass'` `IsScalarTower.right` `Algebra.toSMul` `MulOpposite.instAlgebra` `instFunLike` `symm` `moduleEndSelf` `MulOpposite.op` `LinearMap.instFunLike` `RingHom.id` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	—	`IsScalarTower.to_smulCommClass'` `IsScalarTower.right`
`opComm_apply_apply` 📖	mathematical	—	`DFunLike.coe` `AlgEquiv` `MulOpposite` `MulOpposite.instSemiring` `MulOpposite.instAlgebra` `instFunLike` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `opComm` `MulOpposite.unop`	—	—
`opComm_apply_symm_apply` 📖	mathematical	—	`DFunLike.coe` `AlgEquiv` `MulOpposite` `MulOpposite.instSemiring` `MulOpposite.instAlgebra` `instFunLike` `symm` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `opComm` `MulEquiv` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `MulEquiv.instEquivLike` `MulEquiv.symm` `MulEquivClass.toMulEquiv` `RingEquiv` `Distrib.toAdd` `RingEquiv.instEquivLike` `RingEquivClass.toMulEquivClass` `RingEquiv.instRingEquivClass` `RingEquivClass.toRingEquiv` `instEquivLike` `AlgEquivClass.toRingEquivClass` `instAlgEquivClass` `refl` `trans` `op` `opOp`	—	—
`opComm_symm_apply_apply` 📖	mathematical	—	`DFunLike.coe` `AlgEquiv` `MulOpposite` `MulOpposite.instSemiring` `MulOpposite.instAlgebra` `instFunLike` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `opComm` `MulOpposite.op`	—	—
`opComm_symm_apply_symm_apply` 📖	mathematical	—	`DFunLike.coe` `AlgEquiv` `MulOpposite` `MulOpposite.instSemiring` `MulOpposite.instAlgebra` `instFunLike` `symm` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `opComm` `MulOpposite.unop` `AddEquiv` `MulOpposite.instAdd` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonUnitalSemiring` `AddEquiv.instEquivLike` `AddEquiv.symm` `AddEquivClass.toAddEquiv` `RingEquiv` `MulOpposite.instMul` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `RingEquiv.instEquivLike` `RingEquivClass.toAddEquivClass` `RingEquiv.instRingEquivClass` `RingEquivClass.toRingEquiv` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Distrib.toAdd` `instEquivLike` `AlgEquivClass.toRingEquivClass` `instAlgEquivClass` `trans` `refl` `opOp` `MulOpposite.op`	—	—
`opOp_apply` 📖	mathematical	—	`DFunLike.coe` `AlgEquiv` `MulOpposite` `MulOpposite.instSemiring` `MulOpposite.instAlgebra` `instFunLike` `opOp` `MulOpposite.op`	—	—
`opOp_symm_apply` 📖	mathematical	—	`DFunLike.coe` `AlgEquiv` `MulOpposite` `MulOpposite.instSemiring` `MulOpposite.instAlgebra` `instFunLike` `symm` `opOp` `MulOpposite.unop`	—	—
`op_apply_apply` 📖	mathematical	—	`DFunLike.coe` `AlgEquiv` `MulOpposite` `MulOpposite.instSemiring` `MulOpposite.instAlgebra` `instFunLike` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `op` `MulOpposite.op` `MulOpposite.unop`	—	—
`op_apply_symm_apply` 📖	mathematical	—	`DFunLike.coe` `AlgEquiv` `MulOpposite` `MulOpposite.instSemiring` `MulOpposite.instAlgebra` `instFunLike` `symm` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `op` `MulOpposite.op` `AddEquiv` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `AddEquiv.instEquivLike` `AddEquiv.symm` `AddEquivClass.toAddEquiv` `RingEquiv` `Distrib.toMul` `RingEquiv.instEquivLike` `RingEquivClass.toAddEquivClass` `RingEquiv.instRingEquivClass` `RingEquivClass.toRingEquiv` `instEquivLike` `AlgEquivClass.toRingEquivClass` `instAlgEquivClass` `MulOpposite.unop`	—	—
`op_symm_apply_apply` 📖	mathematical	—	`DFunLike.coe` `AlgEquiv` `instFunLike` `Equiv` `MulOpposite` `MulOpposite.instSemiring` `MulOpposite.instAlgebra` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `op` `MulOpposite.unop` `MulOpposite.op`	—	—
`op_symm_apply_symm_apply` 📖	mathematical	—	`DFunLike.coe` `AlgEquiv` `instFunLike` `symm` `Equiv` `MulOpposite` `MulOpposite.instSemiring` `MulOpposite.instAlgebra` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `op` `MulOpposite.unop` `AddEquiv` `MulOpposite.instAdd` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonUnitalSemiring` `AddEquiv.instEquivLike` `AddEquiv.symm` `AddEquivClass.toAddEquiv` `RingEquiv` `MulOpposite.instMul` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `RingEquiv.instEquivLike` `RingEquivClass.toAddEquivClass` `RingEquiv.instRingEquivClass` `RingEquivClass.toRingEquiv` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Distrib.toAdd` `instEquivLike` `AlgEquivClass.toRingEquivClass` `instAlgEquivClass` `MulOpposite.op`	—	—
`toAlgHom_op` 📖	mathematical	—	`toAlgHom` `MulOpposite` `MulOpposite.instSemiring` `MulOpposite.instAlgebra` `DFunLike.coe` `Equiv` `AlgEquiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `op` `AlgHom` `AlgHom.op`	—	—
`toAlgHom_unop` 📖	mathematical	—	`toAlgHom` `DFunLike.coe` `Equiv` `AlgEquiv` `MulOpposite` `MulOpposite.instSemiring` `MulOpposite.instAlgebra` `EquivLike.toFunLike` `Equiv.instEquivLike` `unop` `AlgHom` `AlgHom.unop`	—	—
`toLinearEquiv_toOpposite` 📖	mathematical	—	`toLinearEquiv` `MulOpposite` `CommSemiring.toSemiring` `MulOpposite.instSemiring` `MulOpposite.instAlgebra` `toOpposite` `MulOpposite.opLinearEquiv` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Algebra.toModule`	—	`RingHomInvPair.ids`
`toOpposite_apply` 📖	mathematical	—	`DFunLike.coe` `AlgEquiv` `MulOpposite` `CommSemiring.toSemiring` `MulOpposite.instSemiring` `MulOpposite.instAlgebra` `instFunLike` `toOpposite` `MulOpposite.op`	—	—
`toOpposite_symm_apply` 📖	mathematical	—	`DFunLike.coe` `AlgEquiv` `MulOpposite` `MulOpposite.instSemiring` `CommSemiring.toSemiring` `MulOpposite.instAlgebra` `instFunLike` `symm` `toOpposite` `MulOpposite.unop`	—	—
`toRingEquiv_op` 📖	mathematical	—	`toRingEquiv` `MulOpposite` `MulOpposite.instSemiring` `MulOpposite.instAlgebra` `DFunLike.coe` `Equiv` `AlgEquiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `op` `RingEquiv` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Distrib.toAdd` `MulOpposite.instMul` `MulOpposite.instAdd` `RingEquiv.op`	—	—
`toRingEquiv_opOp` 📖	mathematical	—	`RingEquivClass.toRingEquiv` `AlgEquiv` `MulOpposite` `MulOpposite.instSemiring` `MulOpposite.instAlgebra` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Distrib.toAdd` `MulOpposite.instMul` `MulOpposite.instAdd` `instEquivLike` `AlgEquivClass.toRingEquivClass` `instAlgEquivClass` `opOp` `RingEquiv.opOp`	—	`AlgEquivClass.toRingEquivClass` `instAlgEquivClass`
`toRingEquiv_toOpposite` 📖	mathematical	—	`RingEquivClass.toRingEquiv` `AlgEquiv` `MulOpposite` `CommSemiring.toSemiring` `MulOpposite.instSemiring` `MulOpposite.instAlgebra` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Distrib.toAdd` `MulOpposite.instMul` `MulOpposite.instAdd` `instEquivLike` `AlgEquivClass.toRingEquivClass` `instAlgEquivClass` `toOpposite` `RingEquiv.toOpposite` `CommSemiring.toNonUnitalCommSemiring`	—	`AlgEquivClass.toRingEquivClass` `instAlgEquivClass`
`toRingEquiv_unop` 📖	mathematical	—	`toRingEquiv` `DFunLike.coe` `Equiv` `AlgEquiv` `MulOpposite` `MulOpposite.instSemiring` `MulOpposite.instAlgebra` `EquivLike.toFunLike` `Equiv.instEquivLike` `unop` `RingEquiv` `MulOpposite.instMul` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonUnitalSemiring` `MulOpposite.instAdd` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `NonUnitalNonAssocSemiring.toAddCommMonoid` `RingEquiv.unop`	—	—

AlgHom

Definitions

Name	Category	Theorems
`fromOpposite` 📖	CompOp	3 math math: `fromOpposite_apply`, `toRingHom_fromOpposite`, `toLinearMap_fromOpposite`
`op` 📖	CompOp	5 math math: `op_apply_apply`, `AlgEquiv.toAlgHom_op`, `CliffordAlgebra.toBaseChange_comp_reverseOp`, `toRingHom_op`, `op_symm_apply_apply`
`opComm` 📖	CompOp	2 math math: `opComm_symm_apply_apply`, `opComm_apply_apply`
`toOpposite` 📖	CompOp	3 math math: `toLinearMap_toOpposite`, `toRingHom_toOpposite`, `toOpposite_apply`
`unop` 📖	CompOp	2 math math: `AlgEquiv.toAlgHom_unop`, `toRingHom_unop`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`fromOpposite_apply` 📖	mathematical	`Commute` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `DFunLike.coe` `AlgHom` `funLike`	`MulOpposite` `MulOpposite.instSemiring` `MulOpposite.instAlgebra` `fromOpposite` `MulOpposite.unop`	—	—
`opComm_apply_apply` 📖	mathematical	—	`DFunLike.coe` `AlgHom` `MulOpposite` `MulOpposite.instSemiring` `MulOpposite.instAlgebra` `funLike` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `opComm` `MulOpposite.unop`	—	—
`opComm_symm_apply_apply` 📖	mathematical	—	`DFunLike.coe` `AlgHom` `MulOpposite` `MulOpposite.instSemiring` `MulOpposite.instAlgebra` `funLike` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `opComm` `MulOpposite.op`	—	—
`op_apply_apply` 📖	mathematical	—	`DFunLike.coe` `AlgHom` `MulOpposite` `MulOpposite.instSemiring` `MulOpposite.instAlgebra` `funLike` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `op` `MulOpposite.op` `MulOpposite.unop`	—	—
`op_symm_apply_apply` 📖	mathematical	—	`DFunLike.coe` `AlgHom` `funLike` `Equiv` `MulOpposite` `MulOpposite.instSemiring` `MulOpposite.instAlgebra` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `op` `MulOpposite.unop` `MulOpposite.op`	—	—
`toLinearMap_fromOpposite` 📖	mathematical	`Commute` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `DFunLike.coe` `AlgHom` `funLike`	`toLinearMap` `MulOpposite` `MulOpposite.instSemiring` `MulOpposite.instAlgebra` `fromOpposite` `LinearMap.comp` `CommSemiring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Algebra.toModule` `RingHom.id` `RingHomCompTriple.ids` `LinearEquiv.toLinearMap` `RingHomInvPair.ids` `MulOpposite.instAddCommMonoid` `MulOpposite.instModule` `LinearEquiv.symm` `MulOpposite.opLinearEquiv`	—	—
`toLinearMap_toOpposite` 📖	mathematical	`Commute` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `DFunLike.coe` `AlgHom` `funLike`	`toLinearMap` `MulOpposite` `MulOpposite.instSemiring` `MulOpposite.instAlgebra` `toOpposite` `LinearMap.comp` `CommSemiring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Algebra.toModule` `RingHom.id` `RingHomCompTriple.ids` `LinearEquiv.toLinearMap` `RingHomInvPair.ids` `MulOpposite.instAddCommMonoid` `MulOpposite.instModule` `MulOpposite.opLinearEquiv`	—	—
`toOpposite_apply` 📖	mathematical	`Commute` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `DFunLike.coe` `AlgHom` `funLike`	`MulOpposite` `MulOpposite.instSemiring` `MulOpposite.instAlgebra` `toOpposite` `MulOpposite.op`	—	—
`toRingHom_fromOpposite` 📖	mathematical	`Commute` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `DFunLike.coe` `AlgHom` `funLike`	`RingHomClass.toRingHom` `MulOpposite` `MulOpposite.instSemiring` `MulOpposite.instAlgebra` `MulOpposite.instNonAssocSemiring` `AlgHomClass.toRingHomClass` `algHomClass` `fromOpposite` `RingHom.fromOpposite`	—	`AlgHomClass.toRingHomClass` `algHomClass`
`toRingHom_op` 📖	mathematical	—	`toRingHom` `MulOpposite` `MulOpposite.instSemiring` `MulOpposite.instAlgebra` `DFunLike.coe` `Equiv` `AlgHom` `EquivLike.toFunLike` `Equiv.instEquivLike` `op` `RingHom` `Semiring.toNonAssocSemiring` `MulOpposite.instNonAssocSemiring` `RingHom.op`	—	—
`toRingHom_toOpposite` 📖	mathematical	`Commute` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `DFunLike.coe` `AlgHom` `funLike`	`RingHomClass.toRingHom` `MulOpposite` `MulOpposite.instSemiring` `MulOpposite.instAlgebra` `MulOpposite.instNonAssocSemiring` `AlgHomClass.toRingHomClass` `algHomClass` `toOpposite` `RingHom.toOpposite`	—	`AlgHomClass.toRingHomClass` `algHomClass`
`toRingHom_unop` 📖	mathematical	—	`toRingHom` `DFunLike.coe` `Equiv` `AlgHom` `MulOpposite` `MulOpposite.instSemiring` `MulOpposite.instAlgebra` `EquivLike.toFunLike` `Equiv.instEquivLike` `unop` `RingHom` `MulOpposite.instNonAssocSemiring` `Semiring.toNonAssocSemiring` `RingHom.unop`	—	—

MulOpposite

Definitions

Name	Category	Theorems
`instAlgebra` 📖	CompOp	140 math math: `CliffordAlgebra.unop_reverseOp`, `AlgEquiv.moduleEndSelfOp_apply_apply`, `Subalgebra.op_toSubsemiring`, `AlgEquiv.opOp_apply`, `Subalgebra.mem_op`, `AlgEquiv.toOpposite_apply`, `Submodule.comap_op_mul`, `Subalgebra.op_sSup`, `TensorAlgebra.toTrivSqZeroExt_ι`, `AlgEquiv.toOpposite_symm_apply`, `Submodule.comap_op_pow`, `Subalgebra.op_sInf`, `Subalgebra.op_bot`, `AlgEquiv.op_apply_apply`, `Submodule.LinearDisjoint.op`, `CliffordAlgebra.op_reverse`, `ExteriorAlgebra.toTrivSqZeroExt_comp_map`, `TrivSqZeroExt.fstHom_comp_map`, `AlgHom.mulLeftRightMatrix.inv_comp`, `TrivSqZeroExt.fst_exp`, `TrivSqZeroExt.map_inr`, `Subalgebra.unop_sup`, `AlgHom.op_apply_apply`, `AlgEquiv.toAlgHom_op`, `AlgEquiv.toLinearEquiv_toOpposite`, `Subalgebra.LinearDisjoint.linearIndependent_left_op_of_flat`, `FormalMultilinearSeries.ofScalarsSum_op`, `AlgHom.toLinearMap_toOpposite`, `algebraMap_apply`, `Submodule.map_unop_mul`, `Subalgebra.mopAlgEquivOp_symm_apply`, `Subalgebra.op_adjoin`, `AlgHom.opComm_symm_apply_apply`, `TrivSqZeroExt.map_comp_inlAlgHom`, `TrivSqZeroExt.eq_smul_exp_of_ne_zero`, `AlgEquiv.op_apply_symm_apply`, `Subalgebra.unop_top`, `AlgEquiv.mopMatrix_apply`, `AlgHom.toRingHom_toOpposite`, `Subalgebra.op_inf`, `Subalgebra.coe_op`, `TrivSqZeroExt.snd_exp`, `TrivSqZeroExt.map_comp_inrHom`, `Algebra.TensorProduct.opAlgEquiv_apply`, `AlgHom.opComm_apply_apply`, `IsAzumaya.mulLeftRight_comp_congr`, `Subalgebra.unop_bot`, `AlgHom.mulLeftRight_apply`, `Subalgebra.linearEquivOp_apply_coe`, `IsAzumaya.bij`, `AlgEquiv.opComm_apply_apply`, `IsSemisimpleRing.exists_algEquiv_pi_matrix_end_mulOpposite`, `Submodule.map_unop_pow`, `Subalgebra.unop_toSubring`, `Submodule.equivOpposite_apply`, `Subalgebra.unop_sSup`, `AlgEquiv.toRingEquiv_unop`, `Subalgebra.unop_le_unop_iff`, `Submodule.map_op_pow`, `CliffordAlgebra.reverseOpEquiv_opComm`, `AlgEquiv.toRingEquiv_opOp`, `Subalgebra.unop_iInf`, `AlgEquiv.op_symm_apply_symm_apply`, `TrivSqZeroExt.exp_def`, `Subalgebra.unop_inf`, `IsAzumaya.coe_tensorEquivEnd`, `AlgHom.fromOpposite_apply`, `ExteriorAlgebra.toTrivSqZeroExt_ι`, `QuaternionAlgebra.coe_starAe`, `IsSimpleRing.exists_algEquiv_matrix_end_mulOpposite`, `Subalgebra.mem_unop`, `Subalgebra.op_top`, `Subalgebra.unop_adjoin`, `Algebra.TensorProduct.opAlgEquiv_symm_apply`, `Subalgebra.op_iInf`, `TrivSqZeroExt.liftEquivOfComm_apply`, `Subalgebra.op_le_iff`, `AlgHom.toRingHom_fromOpposite`, `Submodule.linearDisjoint_op`, `CliffordAlgebra.toBaseChange_comp_reverseOp`, `Submodule.map_op_mul`, `TrivSqZeroExt.sndHom_comp_map`, `TrivSqZeroExt.map_comp_map`, `Subalgebra.algEquivOpMop_apply`, `AlgEquiv.opComm_apply_symm_apply`, `Subalgebra.op_toSubring`, `TrivSqZeroExt.algebraMap_eq_inl`, `AlgHom.toLinearMap_fromOpposite`, `AlgEquiv.toRingEquiv_op`, `AlgEquiv.toAlgHom_unop`, `AlgEquiv.moduleEndSelf_apply_apply`, `Quaternion.coe_starAe`, `TrivSqZeroExt.isUnit_or_isNilpotent_of_isMaximal_isNilpotent`, `AlgHom.toRingHom_unop`, `Subalgebra.op_iSup`, `Algebra.IsCentral.instMulOpposite`, `Subalgebra.op_sup`, `TrivSqZeroExt.snd_map`, `AlgEquiv.moduleEndSelfOp_symm_apply`, `CliffordAlgebra.reverseOp_ι`, `Matrix.transposeAlgEquiv_apply`, `TrivSqZeroExt.fst_map`, `AlgHom.toRingHom_op`, `Subalgebra.unop_toSubsemiring`, `Subalgebra.coe_unop`, `TrivSqZeroExt.liftEquivOfComm_symm_apply_coe`, `AlgEquiv.opComm_symm_apply_apply`, `AlgEquiv.moduleEndSelf_symm_apply`, `Submodule.comap_unop_pow`, `AlgEquiv.opComm_symm_apply_symm_apply`, `TrivSqZeroExt.algebraMap_eq_inlHom`, `Subalgebra.opEquiv_symm_apply`, `Algebra.TensorProduct.opAlgEquiv_tmul`, `AlgEquiv.mopMatrix_symm_apply`, `Subalgebra.linearEquivOp_symm_apply_coe`, `AlgEquiv.toRingEquiv_toOpposite`, `Matrix.transposeAlgEquiv_symm_apply`, `TrivSqZeroExt.map_inl`, `AlgEquiv.op_symm_apply_apply`, `Submodule.equivOpposite_symm_apply`, `Submodule.mulMap_op`, `AlgHom.toOpposite_apply`, `Subalgebra.le_op_iff`, `Algebra.TensorProduct.opAlgEquiv_symm_tmul`, `Subalgebra.mopAlgEquivOp_apply_coe`, `Subalgebra.LinearDisjoint.mulLeftMap_ker_eq_bot_iff_linearIndependent_op`, `Subalgebra.algEquivOpMop_symm_apply_coe`, `AlgHom.op_symm_apply_apply`, `AlgEquiv.opOp_symm_apply`, `CliffordAlgebra.reverseOpEquiv_apply`, `Subalgebra.op_le_op_iff`, `Submodule.comap_unop_mul`, `Subalgebra.opEquiv_apply`, `TrivSqZeroExt.eq_smul_exp_of_invertible`, `TrivSqZeroExt.map_id`, `AlgHom.mulLeftRightMatrix.comp_inv`, `FormalMultilinearSeries.ofScalarsSum_unop`, `IsAzumaya.AlgHom.mulLeftRight_bij`, `Subalgebra.unop_iSup`, `Subalgebra.unop_sInf`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`algebraMap_apply` 📖	mathematical	—	`DFunLike.coe` `RingHom` `MulOpposite` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instSemiring` `RingHom.instFunLike` `algebraMap` `instAlgebra` `op`	—	—

---

← Back to Index