Documentation Verification Report

Maps

📁 Source: Mathlib/Analysis/CStarAlgebra/Unitary/Maps.lean

Statistics

Metric	Count
Definitions `mulLeft`, `mulRight`	2
Theorems `mulLeft_apply`, `mulLeft_mul_apply`, `mulLeft_trans_mulLeft`, `mulRight_apply`, `mulRight_mul_apply`, `mulRight_one`, `mulRight_trans_mulRight`, `symm_mulLeft`, `symm_mulLeft_apply`, `symm_mulRight`, `symm_mulRight_apply`, `toLinearEquiv_mulLeft`, `toLinearEquiv_mulRight`, `toLinearMap_mulRight`	14
Total	16

Unitary

Definitions

Name	Category	Theorems
`mulLeft` 📖	CompOp	6 math math: `mulLeft_trans_mulLeft`, `mulLeft_mul_apply`, `symm_mulLeft`, `mulLeft_apply`, `symm_mulLeft_apply`, `toLinearEquiv_mulLeft`
`mulRight` 📖	CompOp	8 math math: `toLinearMap_mulRight`, `mulRight_trans_mulRight`, `symm_mulRight`, `toLinearEquiv_mulRight`, `mulRight_apply`, `mulRight_mul_apply`, `symm_mulRight_apply`, `mulRight_one`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mulLeft_apply` 📖	mathematical	—	`DFunLike.coe` `LinearIsometryEquiv` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalNormedRing.toNonUnitalSeminormedRing` `NormedRing.toNonUnitalNormedRing` `EquivLike.toFunLike` `LinearIsometryEquiv.instEquivLike` `MonoidHom` `Submonoid` `Monoid.toMulOneClass` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `NormedRing.toRing` `SetLike.instMembership` `Submonoid.instSetLike` `unitary` `StarRing.toStarMul` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonUnitalSemiring` `MulOneClass.toMulOne` `Submonoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `LinearIsometryEquiv.instGroup` `MonoidHom.instFunLike` `mulLeft` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing`	—	`RingHomInvPair.ids`
`mulLeft_mul_apply` 📖	mathematical	—	`DFunLike.coe` `LinearIsometryEquiv` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalNormedRing.toNonUnitalSeminormedRing` `NormedRing.toNonUnitalNormedRing` `EquivLike.toFunLike` `LinearIsometryEquiv.instEquivLike` `MonoidHom` `Submonoid` `Monoid.toMulOneClass` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `NormedRing.toRing` `SetLike.instMembership` `Submonoid.instSetLike` `unitary` `StarRing.toStarMul` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonUnitalSemiring` `MulOneClass.toMulOne` `Submonoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `LinearIsometryEquiv.instGroup` `MonoidHom.instFunLike` `mulLeft` `Submonoid.mul`	—	`RingHomInvPair.ids` `map_mul` `MonoidHomClass.toMulHomClass` `MonoidHom.instMonoidHomClass`
`mulLeft_trans_mulLeft` 📖	mathematical	—	`LinearIsometryEquiv.trans` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `RingHomCompTriple.ids` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalNormedRing.toNonUnitalSeminormedRing` `NormedRing.toNonUnitalNormedRing` `DFunLike.coe` `MonoidHom` `Submonoid` `Monoid.toMulOneClass` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `NormedRing.toRing` `SetLike.instMembership` `Submonoid.instSetLike` `unitary` `StarRing.toStarMul` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonUnitalSemiring` `LinearIsometryEquiv` `MulOneClass.toMulOne` `Submonoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `LinearIsometryEquiv.instGroup` `MonoidHom.instFunLike` `mulLeft` `Submonoid.mul`	—	`RingHomInvPair.ids` `map_mul` `MonoidHomClass.toMulHomClass` `MonoidHom.instMonoidHomClass`
`mulRight_apply` 📖	mathematical	—	`DFunLike.coe` `LinearIsometryEquiv` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalNormedRing.toNonUnitalSeminormedRing` `NormedRing.toNonUnitalNormedRing` `EquivLike.toFunLike` `LinearIsometryEquiv.instEquivLike` `mulRight` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `NormedRing.toRing` `Submonoid` `Monoid.toMulOneClass` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `SetLike.instMembership` `Submonoid.instSetLike` `unitary` `StarRing.toStarMul` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonUnitalSemiring`	—	`RingHomInvPair.ids`
`mulRight_mul_apply` 📖	mathematical	—	`DFunLike.coe` `LinearIsometryEquiv` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalNormedRing.toNonUnitalSeminormedRing` `NormedRing.toNonUnitalNormedRing` `EquivLike.toFunLike` `LinearIsometryEquiv.instEquivLike` `mulRight` `Submonoid` `Monoid.toMulOneClass` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `NormedRing.toRing` `SetLike.instMembership` `Submonoid.instSetLike` `unitary` `StarRing.toStarMul` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonUnitalSemiring` `Submonoid.mul`	—	`RingHomInvPair.ids` `mul_assoc`
`mulRight_one` 📖	mathematical	—	`mulRight` `Submonoid` `Monoid.toMulOneClass` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `NormedRing.toRing` `SetLike.instMembership` `Submonoid.instSetLike` `unitary` `StarRing.toStarMul` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonUnitalSemiring` `Submonoid.one` `LinearIsometryEquiv.refl` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalNormedRing.toNonUnitalSeminormedRing` `NormedRing.toNonUnitalNormedRing`	—	`LinearIsometryEquiv.ext` `RingHomInvPair.ids` `mul_one`
`mulRight_trans_mulRight` 📖	mathematical	—	`LinearIsometryEquiv.trans` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `RingHomCompTriple.ids` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalNormedRing.toNonUnitalSeminormedRing` `NormedRing.toNonUnitalNormedRing` `mulRight` `Submonoid` `Monoid.toMulOneClass` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `NormedRing.toRing` `SetLike.instMembership` `Submonoid.instSetLike` `unitary` `StarRing.toStarMul` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonUnitalSemiring` `Submonoid.mul`	—	`LinearIsometryEquiv.ext` `RingHomInvPair.ids` `RingHomCompTriple.ids` `mul_assoc`
`symm_mulLeft` 📖	mathematical	—	`LinearIsometryEquiv.symm` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalNormedRing.toNonUnitalSeminormedRing` `NormedRing.toNonUnitalNormedRing` `DFunLike.coe` `MonoidHom` `Submonoid` `Monoid.toMulOneClass` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `NormedRing.toRing` `SetLike.instMembership` `Submonoid.instSetLike` `unitary` `StarRing.toStarMul` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonUnitalSemiring` `LinearIsometryEquiv` `MulOneClass.toMulOne` `Submonoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `LinearIsometryEquiv.instGroup` `MonoidHom.instFunLike` `mulLeft` `Star.star` `instStarSubtypeMemSubmonoidUnitary`	—	`LinearIsometryEquiv.ext` `RingHomInvPair.ids`
`symm_mulLeft_apply` 📖	mathematical	—	`DFunLike.coe` `LinearIsometryEquiv` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalNormedRing.toNonUnitalSeminormedRing` `NormedRing.toNonUnitalNormedRing` `EquivLike.toFunLike` `LinearIsometryEquiv.instEquivLike` `LinearIsometryEquiv.symm` `MonoidHom` `Submonoid` `Monoid.toMulOneClass` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `NormedRing.toRing` `SetLike.instMembership` `Submonoid.instSetLike` `unitary` `StarRing.toStarMul` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonUnitalSemiring` `MulOneClass.toMulOne` `Submonoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `LinearIsometryEquiv.instGroup` `MonoidHom.instFunLike` `mulLeft` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Star.star` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `StarRing.toStarAddMonoid`	—	`RingHomInvPair.ids`
`symm_mulRight` 📖	mathematical	—	`LinearIsometryEquiv.symm` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalNormedRing.toNonUnitalSeminormedRing` `NormedRing.toNonUnitalNormedRing` `mulRight` `Star.star` `Submonoid` `Monoid.toMulOneClass` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `NormedRing.toRing` `SetLike.instMembership` `Submonoid.instSetLike` `unitary` `StarRing.toStarMul` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonUnitalSemiring` `instStarSubtypeMemSubmonoidUnitary`	—	`LinearIsometryEquiv.ext` `RingHomInvPair.ids`
`symm_mulRight_apply` 📖	mathematical	—	`DFunLike.coe` `LinearIsometryEquiv` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalNormedRing.toNonUnitalSeminormedRing` `NormedRing.toNonUnitalNormedRing` `EquivLike.toFunLike` `LinearIsometryEquiv.instEquivLike` `LinearIsometryEquiv.symm` `mulRight` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `NormedRing.toRing` `Star.star` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `StarRing.toStarAddMonoid` `Submonoid` `Monoid.toMulOneClass` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `SetLike.instMembership` `Submonoid.instSetLike` `unitary` `StarRing.toStarMul` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonUnitalSemiring`	—	`RingHomInvPair.ids`
`toLinearEquiv_mulLeft` 📖	mathematical	—	`LinearIsometryEquiv.toLinearEquiv` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalNormedRing.toNonUnitalSeminormedRing` `NormedRing.toNonUnitalNormedRing` `DFunLike.coe` `MonoidHom` `Submonoid` `Monoid.toMulOneClass` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `NormedRing.toRing` `SetLike.instMembership` `Submonoid.instSetLike` `unitary` `StarRing.toStarMul` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonUnitalSemiring` `LinearIsometryEquiv` `MulOneClass.toMulOne` `Submonoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `LinearIsometryEquiv.instGroup` `MonoidHom.instFunLike` `mulLeft` `Units` `LinearEquiv` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Units.instMulOneClass` `LinearEquiv.automorphismGroup` `Units.mulLeftLinearEquiv` `toUnits`	—	`RingHomInvPair.ids`
`toLinearEquiv_mulRight` 📖	mathematical	—	`LinearIsometryEquiv.toLinearEquiv` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalNormedRing.toNonUnitalSeminormedRing` `NormedRing.toNonUnitalNormedRing` `mulRight` `Units.mulRightLinearEquiv` `NormedRing.toRing` `DFunLike.coe` `MonoidHom` `Submonoid` `Monoid.toMulOneClass` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `SetLike.instMembership` `Submonoid.instSetLike` `unitary` `StarRing.toStarMul` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonUnitalSemiring` `Units` `MulOneClass.toMulOne` `Submonoid.toMulOneClass` `Units.instMulOneClass` `MonoidHom.instFunLike` `toUnits`	—	`RingHomInvPair.ids`
`toLinearMap_mulRight` 📖	mathematical	—	`LinearEquiv.toLinearMap` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalNormedRing.toNonUnitalSeminormedRing` `NormedRing.toNonUnitalNormedRing` `LinearIsometryEquiv.toLinearEquiv` `mulRight` `LinearMap.mulRight` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `NormedRing.toRing` `Submonoid` `Monoid.toMulOneClass` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `SetLike.instMembership` `Submonoid.instSetLike` `unitary` `StarRing.toStarMul` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonUnitalSemiring`	—	`RingHomInvPair.ids`

---

← Back to Index