UnitaryGroup

📁 Source: Mathlib/LinearAlgebra/UnitaryGroup.lean

Statistics

Metric	Count
Definitions coeFun, coeMatrix, embeddingGL, toGL, toLin', toLinearEquiv, instGroupSubtypeMemSubmonoidSpecialUnitaryGroup, instInvSubtypeMemSubmonoidSpecialUnitaryGroup, instStarMulSubtypeMemSubmonoidSpecialUnitaryGroup, orthogonalGroup, specialOrthogonalGroup, specialUnitaryGroup, unitaryGroup	13
Theorems coe_toGL, det_isUnit, ext, ext_iff, inv_apply, inv_val, mul_apply, mul_val, one_apply, one_val, star_mul_self, toGL_mul, toGL_one, toLin'_mul, toLin'_one, det_of_mem_unitary, kronecker_mem_unitary, 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	28
Total	41

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	24 math math: UnitaryGroup.toLin'_one, UnitaryGroup.toGL_mul, specialUnitaryGroup_le_unitaryGroup, IsHermitian.eigenvectorUnitary_col_eq, IsHermitian.eigenvectorUnitary_mulVec, mem_unitaryGroup_iff, UnitaryGroup.one_apply, UnitaryGroup.one_val, UnitaryGroup.det_isUnit, UnitaryGroup.inv_val, 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', IsHermitian.eigenvectorUnitary_transpose_apply, UnitaryGroup.toLin'_mul, UnitaryGroup.toGL_one, UnitaryGroup.star_mul_self, 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	Monoid.toMulOneClass MonoidWithZero.toMonoid Semiring.toMonoidWithZero unitary StarRing.toStarMul NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring det	—	det_mul det_conjTranspose det_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	instFintypeProd 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
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.toNatPow 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.toNatPow 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	—	—

Matrix.UnitaryGroup

Definitions

Name	Category	Theorems
coeFun 📖	CompOp	—
coeMatrix 📖	CompOp	—
embeddingGL 📖	CompOp	—
toGL 📖	CompOp	3 math math: toGL_mul, coe_toGL, toGL_one
toLin' 📖	CompOp	3 math math: toLin'_one, coe_toGL, toLin'_mul
toLinearEquiv 📖	CompOp	—

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	—	—
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

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	—	—

---

← Back to Index