Documentation Verification Report

UnitaryStarAlgAut

📁 Source: Mathlib/Algebra/Star/UnitaryStarAlgAut.lean

Statistics

Metric	Count
Definitions `conjStarAlgAut`	1
Theorems `conjStarAlgAut_apply`, `conjStarAlgAut_ext_iff`, `conjStarAlgAut_ext_iff'`, `conjStarAlgAut_mul_apply`, `conjStarAlgAut_star_apply`, `conjStarAlgAut_symm`, `conjStarAlgAut_symm_apply`, `conjStarAlgAut_trans_conjStarAlgAut`, `toAlgEquiv_conjStarAlgAut`, `toRingEquiv_conjStarAlgAut`	10
Total	11

Unitary

Definitions

Name	Category	Theorems
`conjStarAlgAut` 📖	CompOp	16 math math: `conjStarAlgAut_trans_conjStarAlgAut`, `conjStarAlgAut_symm`, `conjStarAlgEquiv_unitaryLinearIsometryEquiv`, `conjStarAlgAut_ext_iff'`, `Matrix.IsHermitian.cfcAux_apply`, `conjStarAlgAut_apply`, `toAlgEquiv_conjStarAlgAut`, `conjStarAlgAut_symm_apply`, `toRingEquiv_conjStarAlgAut`, `Matrix.IsHermitian.spectral_theorem`, `conjStarAlgAut_mul_apply`, `Matrix.IsHermitian.star_mul_self_mul_eq_diagonal`, `conjStarAlgAut_symm_unitaryLinearIsometryEquiv`, `Matrix.IsHermitian.conjStarAlgAut_star_eigenvectorUnitary`, `conjStarAlgAut_star_apply`, `conjStarAlgAut_ext_iff`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`conjStarAlgAut_apply` 📖	mathematical	—	`DFunLike.coe` `StarAlgEquiv` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Distrib.toMul` `InvolutiveStar.toStar` `StarMul.toInvolutiveStar` `StarAlgEquiv.instFunLike` `MonoidHom` `Submonoid` `Monoid.toMulOneClass` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `SetLike.instMembership` `Submonoid.instSetLike` `unitary` `MulOneClass.toMulOne` `Submonoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `StarAlgEquiv.aut` `MonoidHom.instFunLike` `conjStarAlgAut` `Star.star`	—	—
`conjStarAlgAut_ext_iff` 📖	mathematical	—	`DFunLike.coe` `MonoidHom` `Submonoid` `Monoid.toMulOneClass` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `SetLike.instMembership` `Submonoid.instSetLike` `unitary` `StarAlgEquiv` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Distrib.toMul` `Algebra.toSMul` `InvolutiveStar.toStar` `StarMul.toInvolutiveStar` `MulOneClass.toMulOne` `Submonoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `StarAlgEquiv.aut` `MonoidHom.instFunLike` `conjStarAlgAut` `IsScalarTower.right` `Algebra.to_smulCommClass`	—	`IsScalarTower.right` `Algebra.to_smulCommClass` `mul_assoc` `Subalgebra.mem_center_iff` `Algebra.IsCentral.center_eq_bot` `Algebra.algebraMap_eq_smul_one` `mul_smul_comm` `mul_one`
`conjStarAlgAut_ext_iff'` 📖	mathematical	—	`DFunLike.coe` `MonoidHom` `Submonoid` `Monoid.toMulOneClass` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `SetLike.instMembership` `Submonoid.instSetLike` `unitary` `StarAlgEquiv` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Distrib.toMul` `Algebra.toSMul` `CommRing.toCommSemiring` `InvolutiveStar.toStar` `StarMul.toInvolutiveStar` `MulOneClass.toMulOne` `Submonoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `StarAlgEquiv.aut` `MonoidHom.instFunLike` `conjStarAlgAut` `IsScalarTower.right` `Algebra.to_smulCommClass` `CommSemiring.toSemiring` `instSMulSubtypeMemSubmonoidUnitary` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Module.toDistribMulAction` `Algebra.toModule`	—	`IsScalarTower.right` `Algebra.to_smulCommClass` `mul_assoc` `Subalgebra.mem_center_iff` `Algebra.IsCentral.center_eq_bot` `Algebra.algebraMap_eq_smul_one` `mul_star_self_of_mem` `one_mul` `Algebra.mul_smul_comm` `mul_one` `StarMul.star_mul` `star_star` `StarModule.star_smul` `star_one` `sub_eq_zero` `smul_eq_zero` `sub_smul` `one_smul` `mul_comm` `smul_zero` `mul_smul_comm` `Submonoid.smulCommClass_left` `star_mul_self_of_mem`
`conjStarAlgAut_mul_apply` 📖	mathematical	—	`DFunLike.coe` `StarAlgEquiv` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Distrib.toMul` `InvolutiveStar.toStar` `StarMul.toInvolutiveStar` `StarAlgEquiv.instFunLike` `MonoidHom` `Submonoid` `Monoid.toMulOneClass` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `SetLike.instMembership` `Submonoid.instSetLike` `unitary` `MulOneClass.toMulOne` `Submonoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `StarAlgEquiv.aut` `MonoidHom.instFunLike` `conjStarAlgAut` `Submonoid.mul`	—	`map_mul` `MonoidHomClass.toMulHomClass` `MonoidHom.instMonoidHomClass`
`conjStarAlgAut_star_apply` 📖	mathematical	—	`DFunLike.coe` `StarAlgEquiv` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Distrib.toMul` `InvolutiveStar.toStar` `StarMul.toInvolutiveStar` `StarAlgEquiv.instFunLike` `MonoidHom` `Submonoid` `Monoid.toMulOneClass` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `SetLike.instMembership` `Submonoid.instSetLike` `unitary` `MulOneClass.toMulOne` `Submonoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `StarAlgEquiv.aut` `MonoidHom.instFunLike` `conjStarAlgAut` `Star.star` `instStarSubtypeMemSubmonoidUnitary`	—	`star_star`
`conjStarAlgAut_symm` 📖	mathematical	—	`StarAlgEquiv.symm` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Distrib.toMul` `InvolutiveStar.toStar` `StarMul.toInvolutiveStar` `DFunLike.coe` `MonoidHom` `Submonoid` `Monoid.toMulOneClass` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `SetLike.instMembership` `Submonoid.instSetLike` `unitary` `StarAlgEquiv` `MulOneClass.toMulOne` `Submonoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `StarAlgEquiv.aut` `MonoidHom.instFunLike` `conjStarAlgAut` `Star.star` `instStarSubtypeMemSubmonoidUnitary`	—	`StarAlgEquiv.ext` `star_star`
`conjStarAlgAut_symm_apply` 📖	mathematical	—	`DFunLike.coe` `StarAlgEquiv` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Distrib.toMul` `InvolutiveStar.toStar` `StarMul.toInvolutiveStar` `StarAlgEquiv.instFunLike` `StarAlgEquiv.symm` `MonoidHom` `Submonoid` `Monoid.toMulOneClass` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `SetLike.instMembership` `Submonoid.instSetLike` `unitary` `MulOneClass.toMulOne` `Submonoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `StarAlgEquiv.aut` `MonoidHom.instFunLike` `conjStarAlgAut` `Star.star`	—	—
`conjStarAlgAut_trans_conjStarAlgAut` 📖	mathematical	—	`StarAlgEquiv.trans` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Distrib.toMul` `InvolutiveStar.toStar` `StarMul.toInvolutiveStar` `DFunLike.coe` `MonoidHom` `Submonoid` `Monoid.toMulOneClass` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `SetLike.instMembership` `Submonoid.instSetLike` `unitary` `StarAlgEquiv` `MulOneClass.toMulOne` `Submonoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `StarAlgEquiv.aut` `MonoidHom.instFunLike` `conjStarAlgAut` `Submonoid.mul`	—	`map_mul` `MonoidHomClass.toMulHomClass` `MonoidHom.instMonoidHomClass`
`toAlgEquiv_conjStarAlgAut` 📖	mathematical	—	`StarAlgEquiv.toAlgEquiv` `InvolutiveStar.toStar` `StarMul.toInvolutiveStar` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `DFunLike.coe` `MonoidHom` `Submonoid` `Monoid.toMulOneClass` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `SetLike.instMembership` `Submonoid.instSetLike` `unitary` `StarAlgEquiv` `Distrib.toAdd` `Algebra.toSMul` `MulOneClass.toMulOne` `Submonoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `StarAlgEquiv.aut` `MonoidHom.instFunLike` `conjStarAlgAut` `IsScalarTower.right` `Algebra.to_smulCommClass` `MulSemiringAction.toAlgEquiv` `ConjAct` `Units` `ConjAct.instGroup` `Units.instGroup` `ConjAct.unitsMulSemiringAction` `ConjAct.unitsSMulCommClass'` `IsScalarTower.to_smulCommClass'` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Semiring.toModule` `Algebra.toModule` `MulEquiv` `MulOne.toMul` `Units.instDivInvMonoid` `ConjAct.instDivInvMonoid` `EquivLike.toFunLike` `MulEquiv.instEquivLike` `ConjAct.toConjAct` `Units.instMulOneClass` `toUnits`	—	`IsScalarTower.right` `Algebra.to_smulCommClass`
`toRingEquiv_conjStarAlgAut` 📖	mathematical	—	`StarRingEquiv.toRingEquiv` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Distrib.toMul` `InvolutiveStar.toStar` `StarMul.toInvolutiveStar` `StarAlgEquiv.toStarRingEquiv` `DFunLike.coe` `MonoidHom` `Submonoid` `Monoid.toMulOneClass` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `SetLike.instMembership` `Submonoid.instSetLike` `unitary` `StarAlgEquiv` `MulOneClass.toMulOne` `Submonoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `StarAlgEquiv.aut` `MonoidHom.instFunLike` `conjStarAlgAut` `MulSemiringAction.toRingEquiv` `ConjAct` `Units` `ConjAct.instGroup` `Units.instGroup` `ConjAct.unitsMulSemiringAction` `MulEquiv` `MulOne.toMul` `Units.instDivInvMonoid` `ConjAct.instDivInvMonoid` `EquivLike.toFunLike` `MulEquiv.instEquivLike` `ConjAct.toConjAct` `Units.instMulOneClass` `toUnits`	—	—

---

← Back to Index