Documentation Verification Report

Opposite

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

Statistics

Metric	Count
Definitions `opLinearEquiv`	1
Theorems `ext_ring_op`, `ext_ring_op_iff`, `coe_opLinearEquiv`, `coe_opLinearEquiv_addEquiv`, `coe_opLinearEquiv_symm`, `coe_opLinearEquiv_symm_addEquiv`, `coe_opLinearEquiv_symm_toLinearMap`, `coe_opLinearEquiv_toLinearMap`, `opLinearEquiv_symm_toAddEquiv`, `opLinearEquiv_toAddEquiv`	10
Total	11

LinearMap

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ext_ring_op` 📖	—	`DFunLike.coe` `LinearMap` `MulOpposite` `MulOpposite.instSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toOppositeModule` `instFunLike` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	—	—	`ext` `one_mul` `op_smul_eq_mul` `map_smulₛₗ`
`ext_ring_op_iff` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `MulOpposite` `MulOpposite.instSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toOppositeModule` `instFunLike` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	—	`ext_ring_op`

MulOpposite

Definitions

Name	Category	Theorems
`opLinearEquiv` 📖	CompOp	33 math math: `coe_opLinearEquiv_symm`, `Submodule.comap_op_mul`, `Submodule.comap_op_pow`, `coe_opLinearEquiv_symm_addEquiv`, `AlgEquiv.toLinearEquiv_toOpposite`, `AlgHom.toLinearMap_toOpposite`, `Submodule.map_unop_mul`, `coe_opLinearEquiv_addEquiv`, `isometry_opLinearEquiv`, `Algebra.TensorProduct.opAlgEquiv_apply`, `Submodule.map_unop_pow`, `Submodule.equivOpposite_apply`, `counit_def`, `coe_opLinearEquiv_toLinearMap`, `Submodule.map_op_pow`, `toLinearEquiv_opLinearIsometryEquiv`, `opLinearEquiv_toAddEquiv`, `Algebra.TensorProduct.opAlgEquiv_symm_apply`, `Submodule.map_op_mul`, `AlgHom.toLinearMap_fromOpposite`, `Submodule.map_unop_one`, `Module.Basis.mulOpposite_repr_eq`, `Submodule.comap_unop_pow`, `coe_opLinearEquiv`, `comul_def`, `opLinearEquiv_symm_toAddEquiv`, `Submodule.equivOpposite_symm_apply`, `Submodule.comap_unop_one`, `Submodule.mulMap_op`, `coe_opLinearEquiv_symm_toLinearMap`, `Submodule.comap_op_one`, `Submodule.map_op_one`, `Submodule.comap_unop_mul`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_opLinearEquiv` 📖	mathematical	—	`DFunLike.coe` `LinearEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `MulOpposite` `instAddCommMonoid` `instModule` `EquivLike.toFunLike` `LinearEquiv.instEquivLike` `opLinearEquiv` `op`	—	`RingHomInvPair.ids`
`coe_opLinearEquiv_addEquiv` 📖	mathematical	—	`AddEquivClass.toAddEquiv` `LinearEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `MulOpposite` `instAddCommMonoid` `instModule` `LinearEquiv.instEquivLike` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `instAdd` `SemilinearEquivClass.toAddEquivClass` `LinearEquiv.instSemilinearEquivClass` `opLinearEquiv` `opAddEquiv`	—	`RingHomInvPair.ids` `SemilinearEquivClass.toAddEquivClass` `LinearEquiv.instSemilinearEquivClass`
`coe_opLinearEquiv_symm` 📖	mathematical	—	`DFunLike.coe` `LinearEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `MulOpposite` `instAddCommMonoid` `instModule` `EquivLike.toFunLike` `LinearEquiv.instEquivLike` `LinearEquiv.symm` `opLinearEquiv` `unop`	—	`RingHomInvPair.ids`
`coe_opLinearEquiv_symm_addEquiv` 📖	mathematical	—	`AddEquivClass.toAddEquiv` `LinearEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `MulOpposite` `instAddCommMonoid` `instModule` `LinearEquiv.instEquivLike` `instAdd` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `SemilinearEquivClass.toAddEquivClass` `LinearEquiv.instSemilinearEquivClass` `LinearEquiv.symm` `opLinearEquiv` `AddEquiv.symm` `opAddEquiv`	—	`RingHomInvPair.ids` `SemilinearEquivClass.toAddEquivClass` `LinearEquiv.instSemilinearEquivClass`
`coe_opLinearEquiv_symm_toLinearMap` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `MulOpposite` `instAddCommMonoid` `instModule` `LinearMap.instFunLike` `LinearEquiv.toLinearMap` `RingHomInvPair.ids` `LinearEquiv.symm` `opLinearEquiv` `unop`	—	`RingHomInvPair.ids`
`coe_opLinearEquiv_toLinearMap` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `MulOpposite` `instAddCommMonoid` `instModule` `LinearMap.instFunLike` `LinearEquiv.toLinearMap` `RingHomInvPair.ids` `opLinearEquiv` `op`	—	`RingHomInvPair.ids`
`opLinearEquiv_symm_toAddEquiv` 📖	mathematical	—	`LinearEquiv.toAddEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `MulOpposite` `instAddCommMonoid` `instModule` `LinearEquiv.symm` `opLinearEquiv` `AddEquiv.symm` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `instAdd` `opAddEquiv`	—	`RingHomInvPair.ids`
`opLinearEquiv_toAddEquiv` 📖	mathematical	—	`LinearEquiv.toAddEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `MulOpposite` `instAddCommMonoid` `instModule` `opLinearEquiv` `opAddEquiv` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup`	—	`RingHomInvPair.ids`

---

← Back to Index