Opposite

📁 Source: Mathlib/LinearAlgebra/TensorProduct/Opposite.lean

Statistics

Metric	Count
Definitions opAlgEquiv	1
Theorems opAlgEquiv_apply, opAlgEquiv_symm_apply, opAlgEquiv_symm_tmul, opAlgEquiv_tmul	4
Total	5

Algebra.TensorProduct

Definitions

Name	Category	Theorems
opAlgEquiv 📖	CompOp	5 math math: opAlgEquiv_apply, opAlgEquiv_symm_apply, CliffordAlgebra.toBaseChange_comp_reverseOp, opAlgEquiv_tmul, opAlgEquiv_symm_tmul

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
opAlgEquiv_apply 📖	mathematical	—	DFunLike.coe AlgEquiv TensorProduct MulOpposite MulOpposite.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring MulOpposite.instModule CommSemiring.toSemiring Algebra.toModule instSemiring MulOpposite.instSemiring MulOpposite.instAlgebra leftAlgebra MulOpposite.instSMulCommClass Algebra.toSMul IsScalarTower.to_smulCommClass AlgEquiv.instFunLike opAlgEquiv MulOpposite.op LinearMap RingHom.id TensorProduct.addCommMonoid TensorProduct.instModule LinearMap.instFunLike TensorProduct.map LinearEquiv.toLinearMap RingHomInvPair.ids LinearEquiv.symm MulOpposite.opLinearEquiv	—	MulOpposite.instSMulCommClass IsScalarTower.to_smulCommClass
opAlgEquiv_symm_apply 📖	mathematical	—	DFunLike.coe AlgEquiv MulOpposite TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule MulOpposite.instAddCommMonoid MulOpposite.instModule CommSemiring.toSemiring MulOpposite.instSemiring instSemiring MulOpposite.instAlgebra leftAlgebra IsScalarTower.to_smulCommClass MulOpposite.instSMulCommClass Algebra.toSMul AlgEquiv.instFunLike AlgEquiv.symm opAlgEquiv LinearMap RingHom.id TensorProduct.addCommMonoid TensorProduct.instModule LinearMap.instFunLike TensorProduct.map LinearEquiv.toLinearMap RingHomInvPair.ids MulOpposite.opLinearEquiv MulOpposite.unop	—	IsScalarTower.to_smulCommClass MulOpposite.instSMulCommClass
opAlgEquiv_symm_tmul 📖	mathematical	—	DFunLike.coe AlgEquiv MulOpposite TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule MulOpposite.instAddCommMonoid MulOpposite.instModule CommSemiring.toSemiring MulOpposite.instSemiring instSemiring MulOpposite.instAlgebra leftAlgebra IsScalarTower.to_smulCommClass MulOpposite.instSMulCommClass Algebra.toSMul AlgEquiv.instFunLike AlgEquiv.symm opAlgEquiv MulOpposite.op TensorProduct.tmul	—	IsScalarTower.to_smulCommClass MulOpposite.instSMulCommClass
opAlgEquiv_tmul 📖	mathematical	—	DFunLike.coe AlgEquiv TensorProduct MulOpposite MulOpposite.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring MulOpposite.instModule CommSemiring.toSemiring Algebra.toModule instSemiring MulOpposite.instSemiring MulOpposite.instAlgebra leftAlgebra MulOpposite.instSMulCommClass Algebra.toSMul IsScalarTower.to_smulCommClass AlgEquiv.instFunLike opAlgEquiv TensorProduct.tmul MulOpposite.op MulOpposite.unop	—	MulOpposite.instSMulCommClass IsScalarTower.to_smulCommClass

---

← Back to Index