Documentation Verification Report

UnitaryGroup

📁 Source: Mathlib/LinearAlgebra/UnitaryGroup.lean

Statistics

Metric	Count
Definitions `coeFun`, `coeMatrix`, `embeddingGL`, `map_star`, `toGL`, `toLin'`, `toLinearEquiv`, `transpose`, `instGroupSubtypeMemSubmonoidSpecialUnitaryGroup`, `instInvSubtypeMemSubmonoidSpecialUnitaryGroup`, `instStarMulSubtypeMemSubmonoidSpecialUnitaryGroup`, `orthogonalGroup`, `specialOrthogonalGroup`, `specialUnitaryGroup`, `unitaryGroup`	15
Theorems `coe_toGL`, `det_isUnit`, `ext`, `ext_iff`, `inv_apply`, `inv_val`, `map_star_coe`, `map_star_inv_eq_transpose`, `mul_apply`, `mul_val`, `one_apply`, `one_val`, `star_mul_self`, `toGL_mul`, `toGL_one`, `toLin'_mul`, `toLin'_one`, `transpose_coe`, `transpose_inv_eq_map_star`, `det_of_mem_unitary`, `kroneckerTMul_mem_unitary`, `kronecker_mem_unitary`, `map_star_mem_unitaryGroup_iff`, `mem_orthogonalGroup_iff`, `mem_orthogonalGroup_iff'`, `mem_specialOrthogonalGroup_fin_two_iff`, `mem_specialOrthogonalGroup_iff`, `mem_specialUnitaryGroup_iff`, `mem_unitaryGroup_iff`, `mem_unitaryGroup_iff'`, `of_mem_specialOrthogonalGroup_fin_two_iff`, `coe_star`, `specialUnitaryGroup_le_unitaryGroup`, `star_eq_inv`, `transpose_mem_unitaryGroup_iff`, `tmul_mem`	36
Total	51

Matrix

Definitions

Name	Category	Theorems
`instGroupSubtypeMemSubmonoidSpecialUnitaryGroup` 📖	CompOp	—
`instInvSubtypeMemSubmonoidSpecialUnitaryGroup` 📖	CompOp	1 math math: `star_eq_inv`
`instStarMulSubtypeMemSubmonoidSpecialUnitaryGroup` 📖	CompOp	2 math math: `star_eq_inv`, `specialUnitaryGroup.coe_star`
`orthogonalGroup` 📖	CompOp	4 math math: `mem_specialOrthogonalGroup_iff`, `mem_orthogonalGroup_iff`, `mem_orthogonalGroup_iff'`, `OrthonormalBasis.toMatrix_orthonormalBasis_mem_orthogonal`
`specialOrthogonalGroup` 📖	CompOp	3 math math: `mem_specialOrthogonalGroup_iff`, `of_mem_specialOrthogonalGroup_fin_two_iff`, `mem_specialOrthogonalGroup_fin_two_iff`
`specialUnitaryGroup` 📖	CompOp	4 math math: `specialUnitaryGroup_le_unitaryGroup`, `mem_specialUnitaryGroup_iff`, `star_eq_inv`, `specialUnitaryGroup.coe_star`
`unitaryGroup` 📖	CompOp	31 math math: `UnitaryGroup.toLin'_one`, `UnitaryGroup.toGL_mul`, `specialUnitaryGroup_le_unitaryGroup`, `IsHermitian.eigenvectorUnitary_col_eq`, `IsHermitian.eigenvectorUnitary_mulVec`, `mem_unitaryGroup_iff`, `map_star_mem_unitaryGroup_iff`, `UnitaryGroup.map_star_inv_eq_transpose`, `UnitaryGroup.one_apply`, `UnitaryGroup.one_val`, `UnitaryGroup.det_isUnit`, `UnitaryGroup.inv_val`, `UnitaryGroup.transpose_coe`, `mem_specialUnitaryGroup_iff`, `UnitaryGroup.mul_val`, `IsHermitian.eigenvectorUnitary_apply`, `UnitaryGroup.mul_apply`, `UnitaryGroup.ext_iff`, `IsHermitian.eigenvectorUnitary_coe`, `OrthonormalBasis.toMatrix_orthonormalBasis_mem_unitary`, `mem_unitaryGroup_iff'`, `transpose_mem_unitaryGroup_iff`, `UnitaryGroup.map_star_coe`, `IsHermitian.eigenvectorUnitary_transpose_apply`, `LinearIsometryEquiv.toMatrix_mem_unitaryGroup`, `UnitaryGroup.toLin'_mul`, `UnitaryGroup.toGL_one`, `UnitaryGroup.star_mul_self`, `UnitaryGroup.transpose_inv_eq_map_star`, `IsHermitian.star_eigenvectorUnitary_mulVec`, `UnitaryGroup.inv_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`det_of_mem_unitary` 📖	mathematical	`Matrix` `Submonoid` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `nonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `SetLike.instMembership` `Submonoid.instSetLike` `unitaryGroup`	`Submonoid` `Monoid.toMulOneClass` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `SetLike.instMembership` `Submonoid.instSetLike` `unitary` `StarRing.toStarMul` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonUnitalSemiring` `det`	—	`det_mul` `det_conjTranspose` `det_one`
`kroneckerTMul_mem_unitary` 📖	mathematical	`Matrix` `Submonoid` `Monoid.toMulOneClass` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `semiring` `SetLike.instMembership` `Submonoid.instSetLike` `unitary` `StarRing.toStarMul` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonUnitalSemiring` `instStarRing`	`Matrix` `TensorProduct` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Algebra.toModule` `Submonoid` `Monoid.toMulOneClass` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `semiring` `Algebra.TensorProduct.instSemiring` `instFintypeProd` `SetLike.instMembership` `Submonoid.instSetLike` `unitary` `StarRing.toStarMul` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonUnitalSemiring` `instStarRing` `Algebra.TensorProduct.instNonUnitalSemiring` `Algebra.to_smulCommClass` `IsScalarTower.right` `TensorProduct.instStarRing` `kroneckerMap` `TensorProduct.tmul`	—	`Algebra.to_smulCommClass` `IsScalarTower.right` `conjTranspose_kroneckerTMul` `one_kroneckerTMul_one`
`kronecker_mem_unitary` 📖	mathematical	`Matrix` `Submonoid` `Monoid.toMulOneClass` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `semiring` `SetLike.instMembership` `Submonoid.instSetLike` `unitary` `StarRing.toStarMul` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonUnitalSemiring` `instStarRing`	`Matrix` `Submonoid` `Monoid.toMulOneClass` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `semiring` `instFintypeProd` `SetLike.instMembership` `Submonoid.instSetLike` `unitary` `StarRing.toStarMul` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonUnitalSemiring` `instStarRing` `kroneckerMap` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	—	`conjTranspose_kronecker'` `ext` `Finset.sum_congr` `mul_assoc` `Finset.sum_product` `Finset.sum_comm` `mul_boole` `ite_mul` `MulZeroClass.zero_mul` `Finset.sum_ite_irrel` `Finset.sum_const_zero`
`map_star_mem_unitaryGroup_iff` 📖	mathematical	—	`Matrix` `Submonoid` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `nonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `SetLike.instMembership` `Submonoid.instSetLike` `unitaryGroup` `map` `Star.star` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `StarRing.toStarAddMonoid`	—	—
`mem_orthogonalGroup_iff` 📖	mathematical	—	`Matrix` `Submonoid` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `nonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `SetLike.instMembership` `Submonoid.instSetLike` `orthogonalGroup` `instHMulOfFintypeOfMulOfAddCommMonoid` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `NonUnitalNonAssocSemiring.toAddCommMonoid` `transpose` `one` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing`	—	`mem_unitaryGroup_iff`
`mem_orthogonalGroup_iff'` 📖	mathematical	—	`Matrix` `Submonoid` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `nonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `SetLike.instMembership` `Submonoid.instSetLike` `orthogonalGroup` `instHMulOfFintypeOfMulOfAddCommMonoid` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `NonUnitalNonAssocSemiring.toAddCommMonoid` `transpose` `one` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing`	—	`mem_unitaryGroup_iff'`
`mem_specialOrthogonalGroup_fin_two_iff` 📖	mathematical	—	`Matrix` `Submonoid` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `nonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Fin.fintype` `SetLike.instMembership` `Submonoid.instSetLike` `specialOrthogonalGroup` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `CommRing.toRing` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Monoid.toPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne`	—	`etaExpand_eq` `of_mem_specialOrthogonalGroup_fin_two_iff`
`mem_specialOrthogonalGroup_iff` 📖	mathematical	—	`Matrix` `Submonoid` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `nonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `SetLike.instMembership` `Submonoid.instSetLike` `specialOrthogonalGroup` `orthogonalGroup` `det` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing`	—	—
`mem_specialUnitaryGroup_iff` 📖	mathematical	—	`Matrix` `Submonoid` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `nonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `SetLike.instMembership` `Submonoid.instSetLike` `specialUnitaryGroup` `unitaryGroup` `det` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing`	—	—
`mem_unitaryGroup_iff` 📖	mathematical	—	`Matrix` `Submonoid` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `nonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `SetLike.instMembership` `Submonoid.instSetLike` `unitaryGroup` `instHMulOfFintypeOfMulOfAddCommMonoid` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Star.star` `instStar` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `StarRing.toStarAddMonoid` `one` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing`	—	`instIsDedekindFiniteMonoidOfIsStablyFiniteRing` `instIsStablyFiniteRingOfCommSemiring`
`mem_unitaryGroup_iff'` 📖	mathematical	—	`Matrix` `Submonoid` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `nonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `SetLike.instMembership` `Submonoid.instSetLike` `unitaryGroup` `instHMulOfFintypeOfMulOfAddCommMonoid` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Star.star` `instStar` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `StarRing.toStarAddMonoid` `one` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing`	—	`mul_eq_one_comm` `instIsDedekindFiniteMonoidOfIsStablyFiniteRing` `instIsStablyFiniteRingOfCommSemiring`
`of_mem_specialOrthogonalGroup_fin_two_iff` 📖	mathematical	—	`Matrix` `Submonoid` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `nonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Fin.fintype` `SetLike.instMembership` `Submonoid.instSetLike` `specialOrthogonalGroup` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `of` `vecCons` `vecEmpty` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `CommRing.toRing` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Monoid.toPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne`	—	`cons_transpose` `cons_mul` `cons_vecMul` `smul_cons` `cons_val_fin_one` `add_zero` `add_cons` `empty_mul` `Equiv.symm_apply_apply` `cons_val'` `cons_val_succ` `Fin.isEmpty'` `one_apply_eq` `one_apply_ne` `Fin.instNeZeroHAddNatOfNat_mathlib_1` `det_fin_two_of`
`specialUnitaryGroup_le_unitaryGroup` 📖	mathematical	—	`Submonoid` `Matrix` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `nonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Preorder.toLE` `PartialOrder.toPreorder` `Submonoid.instPartialOrder` `specialUnitaryGroup` `unitaryGroup`	—	`inf_le_left`
`star_eq_inv` 📖	mathematical	—	`Star.star` `Matrix` `Submonoid` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `nonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `SetLike.instMembership` `Submonoid.instSetLike` `specialUnitaryGroup` `InvolutiveStar.toStar` `StarMul.toInvolutiveStar` `Submonoid.mul` `instStarMulSubtypeMemSubmonoidSpecialUnitaryGroup` `instInvSubtypeMemSubmonoidSpecialUnitaryGroup`	—	—
`transpose_mem_unitaryGroup_iff` 📖	mathematical	—	`Matrix` `Submonoid` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `nonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `SetLike.instMembership` `Submonoid.instSetLike` `unitaryGroup` `transpose`	—	`mem_unitaryGroup_iff'` `mem_unitaryGroup_iff` `transpose_mul` `transpose_transpose` `transpose_one`

Matrix.UnitaryGroup

Definitions

Name	Category	Theorems
`coeFun` 📖	CompOp	—
`coeMatrix` 📖	CompOp	—
`embeddingGL` 📖	CompOp	—
`map_star` 📖	CompOp	3 math math: `map_star_inv_eq_transpose`, `map_star_coe`, `transpose_inv_eq_map_star`
`toGL` 📖	CompOp	3 math math: `toGL_mul`, `coe_toGL`, `toGL_one`
`toLin'` 📖	CompOp	3 math math: `toLin'_one`, `coe_toGL`, `toLin'_mul`
`toLinearEquiv` 📖	CompOp	—
`transpose` 📖	CompOp	3 math math: `map_star_inv_eq_transpose`, `transpose_coe`, `transpose_inv_eq_map_star`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_toGL` 📖	mathematical	—	`Units.val` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `Pi.addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Pi.Function.module` `Semiring.toModule` `Module.End.instMonoid` `toGL` `toLin'`	—	—
`det_isUnit` 📖	mathematical	—	`IsUnit` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Matrix.det` `Matrix` `Submonoid` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Matrix.nonAssocSemiring` `Semiring.toNonAssocSemiring` `SetLike.instMembership` `Submonoid.instSetLike` `Matrix.unitaryGroup`	—	`Matrix.isUnit_iff_isUnit_det` `Units.isUnit`
`ext` 📖	—	`Matrix` `Submonoid` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Matrix.nonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `SetLike.instMembership` `Submonoid.instSetLike` `Matrix.unitaryGroup`	—	—	`ext_iff`
`ext_iff` 📖	mathematical	—	`Matrix` `Submonoid` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Matrix.nonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `SetLike.instMembership` `Submonoid.instSetLike` `Matrix.unitaryGroup`	—	`Matrix.ext`
`inv_apply` 📖	mathematical	—	`Matrix` `Submonoid` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Matrix.nonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `SetLike.instMembership` `Submonoid.instSetLike` `Matrix.unitaryGroup` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `Unitary.instGroupSubtypeMemSubmonoidUnitary` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Matrix.semiring` `StarRing.toStarMul` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonUnitalSemiring` `Matrix.instStarRing` `NonUnitalCommSemiring.toNonUnitalSemiring` `NonUnitalCommRing.toNonUnitalCommSemiring` `CommRing.toNonUnitalCommRing` `Star.star` `Matrix.instStar` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `StarRing.toStarAddMonoid`	—	—
`inv_val` 📖	mathematical	—	`Matrix` `Submonoid` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Matrix.nonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `SetLike.instMembership` `Submonoid.instSetLike` `Matrix.unitaryGroup` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `Unitary.instGroupSubtypeMemSubmonoidUnitary` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Matrix.semiring` `StarRing.toStarMul` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonUnitalSemiring` `Matrix.instStarRing` `NonUnitalCommSemiring.toNonUnitalSemiring` `NonUnitalCommRing.toNonUnitalCommSemiring` `CommRing.toNonUnitalCommRing` `Star.star` `Matrix.instStar` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `StarRing.toStarAddMonoid`	—	—
`map_star_coe` 📖	mathematical	—	`Matrix` `Submonoid` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Matrix.nonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `SetLike.instMembership` `Submonoid.instSetLike` `Matrix.unitaryGroup` `map_star` `Matrix.map` `Star.star` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `StarRing.toStarAddMonoid`	—	—
`map_star_inv_eq_transpose` 📖	mathematical	—	`Matrix` `Submonoid` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Matrix.nonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `SetLike.instMembership` `Submonoid.instSetLike` `Matrix.unitaryGroup` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `Unitary.instGroupSubtypeMemSubmonoidUnitary` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Matrix.semiring` `StarRing.toStarMul` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonUnitalSemiring` `Matrix.instStarRing` `NonUnitalCommSemiring.toNonUnitalSemiring` `NonUnitalCommRing.toNonUnitalCommSemiring` `CommRing.toNonUnitalCommRing` `map_star` `transpose`	—	`ext` `star_star`
`mul_apply` 📖	mathematical	—	`Matrix` `Submonoid` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Matrix.nonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `SetLike.instMembership` `Submonoid.instSetLike` `Matrix.unitaryGroup` `Submonoid.mul` `Matrix.instHMulOfFintypeOfMulOfAddCommMonoid` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `NonUnitalNonAssocSemiring.toAddCommMonoid`	—	—
`mul_val` 📖	mathematical	—	`Matrix` `Submonoid` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Matrix.nonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `SetLike.instMembership` `Submonoid.instSetLike` `Matrix.unitaryGroup` `Submonoid.mul` `Matrix.instHMulOfFintypeOfMulOfAddCommMonoid` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `NonUnitalNonAssocSemiring.toAddCommMonoid`	—	—
`one_apply` 📖	mathematical	—	`Matrix` `Submonoid` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Matrix.nonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `SetLike.instMembership` `Submonoid.instSetLike` `Matrix.unitaryGroup` `Submonoid.one` `Matrix.one` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing`	—	—
`one_val` 📖	mathematical	—	`Matrix` `Submonoid` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Matrix.nonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `SetLike.instMembership` `Submonoid.instSetLike` `Matrix.unitaryGroup` `Submonoid.one` `Matrix.one` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing`	—	—
`star_mul_self` 📖	mathematical	—	`Matrix` `Matrix.instHMulOfFintypeOfMulOfAddCommMonoid` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Star.star` `Matrix.instStar` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `StarRing.toStarAddMonoid` `Submonoid` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Matrix.nonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `SetLike.instMembership` `Submonoid.instSetLike` `Matrix.unitaryGroup` `Matrix.one` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing`	—	—
`toGL_mul` 📖	mathematical	—	`toGL` `Matrix` `Submonoid` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Matrix.nonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `SetLike.instMembership` `Submonoid.instSetLike` `Matrix.unitaryGroup` `Submonoid.mul` `LinearMap.GeneralLinearGroup` `Pi.addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Pi.Function.module` `Semiring.toModule` `Units.instMul` `LinearMap` `RingHom.id` `Module.End.instMonoid`	—	`Units.ext` `RingHomCompTriple.ids` `toLin'_mul`
`toGL_one` 📖	mathematical	—	`toGL` `Matrix` `Submonoid` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Matrix.nonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `SetLike.instMembership` `Submonoid.instSetLike` `Matrix.unitaryGroup` `Submonoid.one` `LinearMap.GeneralLinearGroup` `Pi.addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Pi.Function.module` `Semiring.toModule` `Units.instOne` `LinearMap` `RingHom.id` `Module.End.instMonoid`	—	`Units.ext` `toLin'_one`
`toLin'_mul` 📖	mathematical	—	`toLin'` `Matrix` `Submonoid` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Matrix.nonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `SetLike.instMembership` `Submonoid.instSetLike` `Matrix.unitaryGroup` `Submonoid.mul` `LinearMap.comp` `Pi.addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Pi.Function.module` `Semiring.toModule` `RingHom.id` `RingHomCompTriple.ids`	—	`Matrix.toLin'_mul`
`toLin'_one` 📖	mathematical	—	`toLin'` `Matrix` `Submonoid` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Matrix.nonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `SetLike.instMembership` `Submonoid.instSetLike` `Matrix.unitaryGroup` `Submonoid.one` `LinearMap.id` `Pi.addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Pi.Function.module` `Semiring.toModule`	—	`Matrix.toLin'_one`
`transpose_coe` 📖	mathematical	—	`Matrix` `Submonoid` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Matrix.nonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `SetLike.instMembership` `Submonoid.instSetLike` `Matrix.unitaryGroup` `transpose` `Matrix.transpose`	—	—
`transpose_inv_eq_map_star` 📖	mathematical	—	`Matrix` `Submonoid` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Matrix.nonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `SetLike.instMembership` `Submonoid.instSetLike` `Matrix.unitaryGroup` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `Unitary.instGroupSubtypeMemSubmonoidUnitary` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Matrix.semiring` `StarRing.toStarMul` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonUnitalSemiring` `Matrix.instStarRing` `NonUnitalCommSemiring.toNonUnitalSemiring` `NonUnitalCommRing.toNonUnitalCommSemiring` `CommRing.toNonUnitalCommRing` `transpose` `map_star`	—	`inv_inv`

Matrix.specialUnitaryGroup

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_star` 📖	mathematical	—	`Matrix` `Submonoid` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Matrix.nonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `SetLike.instMembership` `Submonoid.instSetLike` `Matrix.specialUnitaryGroup` `Star.star` `InvolutiveStar.toStar` `StarMul.toInvolutiveStar` `Submonoid.mul` `Matrix.instStarMulSubtypeMemSubmonoidSpecialUnitaryGroup` `Matrix.instStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `StarRing.toStarAddMonoid`	—	—

Unitary

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`tmul_mem` 📖	mathematical	`Submonoid` `Monoid.toMulOneClass` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `SetLike.instMembership` `Submonoid.instSetLike` `unitary` `StarRing.toStarMul` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonUnitalSemiring`	`TensorProduct` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Algebra.toModule` `Submonoid` `Monoid.toMulOneClass` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Algebra.TensorProduct.instSemiring` `SetLike.instMembership` `Submonoid.instSetLike` `unitary` `TensorProduct.instStarMul` `Algebra.to_smulCommClass` `IsScalarTower.right` `TensorProduct.tmul`	—	`Algebra.to_smulCommClass` `IsScalarTower.right` `star_mul_self_of_mem` `mul_star_self_of_mem`

---

← Back to Index