Unitary

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

Statistics

Metric	Count
Definitions `instCommGroupSubtypeMemSubmonoidUnitary`, `instGroupSubtypeMemSubmonoidUnitary`, `instHasDistribNegSubtypeMemSubmonoidUnitary`, `instInhabitedSubtypeMemSubmonoidUnitary`, `instInvolutiveStarSubtypeMemSubmonoidUnitary`, `instMulActionSubtypeMemSubmonoidUnitary`, `instNegSubtypeMemSubmonoidUnitary`, `instSMulSubtypeMemSubmonoidUnitary`, `instStarMulSubtypeMemSubmonoidUnitary`, `instStarSubtypeMemSubmonoidUnitary`, `map`, `mapEquiv`, `toUnits`, `unitary`, `map`, `mapEquiv`, `toUnits`, `unitarySubgroup`, `unitarySubgroupUnitsEquiv`	19
Theorems `two_mul_sub_one_mem_unitary`, `mem_unitary_iff_mul_star_self`, `mem_unitary_iff_star_mul_self`, `mem_unitary_of_mul_star_self`, `mem_unitary_of_star_mul_self`, `coe_div`, `coe_inv`, `coe_isStarNormal`, `coe_map`, `coe_map_star`, `coe_mul_star_self`, `coe_neg`, `coe_smul`, `coe_star`, `coe_star_mul_self`, `coe_zpow`, `instIsScalarTowerSubtypeMemSubmonoidUnitary`, `instIsStarNormal`, `instSMulCommClassSubtypeMemSubmonoidUnitary`, `instStarModuleSubtypeMemSubmonoidUnitary`, `inv_mem`, `inv_mem_iff`, `inv_mul_mem_iff`, `isUnit_coe`, `mapEquiv_apply`, `mapEquiv_refl`, `mapEquiv_symm`, `mapEquiv_symm_apply`, `mapEquiv_trans`, `map_coe`, `map_comp`, `map_id`, `map_injective`, `map_mem`, `mem_iff`, `mem_iff_self_mul_star`, `mem_iff_star_mul_self`, `mul_inv_mem_iff`, `mul_left_inj`, `mul_right_inj`, `mul_star_self`, `mul_star_self_of_mem`, `smul_mem`, `smul_mem_of_mem`, `spectrum_star_left_conjugate`, `spectrum_star_right_conjugate`, `star_eq_inv`, `star_eq_inv'`, `star_mem`, `star_mem_iff`, `star_mul_self`, `star_mul_self_of_mem`, `toMonoidHom_mapEquiv`, `toUnits_comp_map`, `toUnits_injective`, `val_inv_toUnits_apply`, `val_toUnits_apply`, `inv_mul_mem_unitary`, `mul_inv_mem_unitary`, `unitary_eq`, `isStarNormal_of_mem_unitary`, `mem_unitarySubgroup_iff`, `coe_div`, `coe_inv`, `coe_map`, `coe_map_star`, `coe_mul_star_self`, `coe_neg`, `coe_smul`, `coe_star`, `coe_star_mul_self`, `coe_zpow`, `inv_mem`, `inv_mul_mem_iff`, `mapEquiv_refl`, `mapEquiv_symm`, `mapEquiv_trans`, `map_comp`, `map_id`, `map_injective`, `map_mem`, `mem_iff`, `mem_iff_self_mul_star`, `mem_iff_star_mul_self`, `mul_inv_mem_iff`, `mul_left_inj`, `mul_right_inj`, `mul_star_self`, `mul_star_self_of_mem`, `smul_mem`, `smul_mem_of_mem`, `unitary_conjugate`, `unitary_conjugate'`, `star_eq_inv`, `star_eq_inv'`, `star_mem`, `star_mem_iff`, `star_mul_self`, `star_mul_self_of_mem`, `toMonoidHom_mapEquiv`, `toUnits_comp_map`, `toUnits_injective`, `val_toUnits_apply`, `unitarySubgroupUnitsEquiv_apply_coe`, `unitarySubgroup_toSubmonoid`, `val_inv_unitarySubgroupUnitsEquiv_symm_apply_coe`, `val_unitarySubgroupUnitsEquiv_symm_apply_coe`	107
Total	126

IsStarProjection

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`two_mul_sub_one_mem_unitary` 📖	mathematical	`IsStarProjection` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `StarRing.toStarAddMonoid`	`Submonoid` `Monoid.toMulOneClass` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `SetLike.instMembership` `Submonoid.instSetLike` `unitary` `StarRing.toStarMul` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonUnitalSemiring` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Nat.instAtLeastTwoHAddOfNat` `AddMonoidWithOne.toOne`	—	`Nat.instAtLeastTwoHAddOfNat` `two_mul` `star_sub` `StarAddMonoid.star_add` `IsSelfAdjoint.star_eq` `isSelfAdjoint` `star_one` `mul_sub` `mul_add` `Distrib.leftDistribClass` `sub_mul` `add_mul` `Distrib.rightDistribClass` `IsIdempotentElem.eq` `isIdempotentElem` `one_mul` `add_sub_cancel_right` `mul_one` `sub_sub_cancel`

IsUnit

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mem_unitary_iff_mul_star_self` 📖	mathematical	`IsUnit`	`Submonoid` `Monoid.toMulOneClass` `SetLike.instMembership` `Submonoid.instSetLike` `unitary` `MulOne.toMul` `MulOneClass.toMulOne` `Star.star` `InvolutiveStar.toStar` `StarMul.toInvolutiveStar` `MulOne.toOne`	—	`Unitary.star_mem_iff` `mem_unitary_iff_star_mul_self` `star` `star_star`
`mem_unitary_iff_star_mul_self` 📖	mathematical	`IsUnit`	`Submonoid` `Monoid.toMulOneClass` `SetLike.instMembership` `Submonoid.instSetLike` `unitary` `MulOne.toMul` `MulOneClass.toMulOne` `Star.star` `InvolutiveStar.toStar` `StarMul.toInvolutiveStar` `MulOne.toOne`	—	`Unitary.mem_iff` `CanLift.prf` `instCanLiftUnitsValIsUnit` `Units.mul_inv` `left_inv_eq_right_inv`
`mem_unitary_of_mul_star_self` 📖	mathematical	`IsUnit` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `Star.star` `InvolutiveStar.toStar` `StarMul.toInvolutiveStar` `MulOne.toOne`	`Submonoid` `SetLike.instMembership` `Submonoid.instSetLike` `unitary`	—	`mem_unitary_iff_mul_star_self`
`mem_unitary_of_star_mul_self` 📖	mathematical	`IsUnit` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `Star.star` `InvolutiveStar.toStar` `StarMul.toInvolutiveStar` `MulOne.toOne`	`Submonoid` `SetLike.instMembership` `Submonoid.instSetLike` `unitary`	—	`mem_unitary_iff_star_mul_self`

Unitary

Definitions

Name	Category	Theorems
`instCommGroupSubtypeMemSubmonoidUnitary` 📖	CompOp	2 math math: `LinearIsometryEquiv.symm_units_smul`, `LinearIsometryEquiv.symm_smul_apply`
`instGroupSubtypeMemSubmonoidUnitary` 📖	CompOp	15 math math: `unitary.star_eq_inv'`, `coe_zpow`, `unitary.coe_div`, `unitary.coe_zpow`, `instIsTopologicalGroupSubtypeMemSubmonoidUnitaryOfContinuousMulOfContinuousStar`, `Matrix.UnitaryGroup.inv_val`, `unitary.coe_inv`, `coe_div`, `val_inv_toUnits_apply`, `star_eq_inv`, `instContinuousInvSubtypeMemSubmonoidUnitaryOfContinuousStar`, `unitary.star_eq_inv`, `star_eq_inv'`, `coe_inv`, `Matrix.UnitaryGroup.inv_apply`
`instHasDistribNegSubtypeMemSubmonoidUnitary` 📖	CompOp	—
`instInhabitedSubtypeMemSubmonoidUnitary` 📖	CompOp	—
`instInvolutiveStarSubtypeMemSubmonoidUnitary` 📖	CompOp	—
`instMulActionSubtypeMemSubmonoidUnitary` 📖	CompOp	—
`instNegSubtypeMemSubmonoidUnitary` 📖	CompOp	2 math math: `coe_neg`, `unitary.coe_neg`
`instSMulSubtypeMemSubmonoidUnitary` 📖	CompOp	6 math math: `unitary.coe_smul`, `conjStarAlgAut_ext_iff'`, `coe_smul`, `instSMulCommClassSubtypeMemSubmonoidUnitary`, `instIsScalarTowerSubtypeMemSubmonoidUnitary`, `instStarModuleSubtypeMemSubmonoidUnitary`
`instStarMulSubtypeMemSubmonoidUnitary` 📖	CompOp	—
`instStarSubtypeMemSubmonoidUnitary` 📖	CompOp	48 math math: `unitary.star_eq_inv'`, `conjStarAlgAut_symm`, `unitary.map_id`, `mapEquiv_symm_apply`, `unitary.map_comp`, `unitary.mapEquiv_trans`, `map_coe`, `unitary.toUnits_comp_map`, `expUnitary_eq_mul_inv`, `unitary.norm_sub_eq`, `coe_mul_star_self`, `mul_star_self`, `map_comp`, `mapEquiv_apply`, `CStarAlgebra.norm_smul_two_inv_smul_add_four_unitary`, `star_mul_self`, `instIsStarNormal`, `unitary.mapEquiv_symm`, `unitary.coe_mul_star_self`, `unitary.coe_map`, `toUnits_comp_map`, `coe_map_star`, `unitary.coe_map_star`, `map_injective`, `mapEquiv_symm`, `instContinuousStarSubtypeMemSubmonoidUnitary`, `unitary.toMonoidHom_mapEquiv`, `map_id`, `mapEquiv_trans`, `norm_sub_eq`, `unitary.coe_star`, `coe_map`, `unitary.expUnitary_eq_mul_inv`, `unitary.mapEquiv_refl`, `Matrix.IsHermitian.star_mul_self_mul_eq_diagonal`, `star_eq_inv`, `unitary.map_injective`, `instStarModuleSubtypeMemSubmonoidUnitary`, `toMonoidHom_mapEquiv`, `Matrix.IsHermitian.conjStarAlgAut_star_eigenvectorUnitary`, `unitary.mul_star_self`, `coe_star`, `conjStarAlgAut_star_apply`, `unitary.star_eq_inv`, `mapEquiv_refl`, `star_eq_inv'`, `path_apply`, `unitary.star_mul_self`
`map` 📖	CompOp	17 math math: `unitary.map_id`, `mapEquiv_symm_apply`, `unitary.map_comp`, `map_coe`, `unitary.toUnits_comp_map`, `map_comp`, `mapEquiv_apply`, `unitary.coe_map`, `toUnits_comp_map`, `coe_map_star`, `unitary.coe_map_star`, `map_injective`, `unitary.toMonoidHom_mapEquiv`, `map_id`, `coe_map`, `unitary.map_injective`, `toMonoidHom_mapEquiv`
`mapEquiv` 📖	CompOp	10 math math: `mapEquiv_symm_apply`, `unitary.mapEquiv_trans`, `mapEquiv_apply`, `unitary.mapEquiv_symm`, `mapEquiv_symm`, `unitary.toMonoidHom_mapEquiv`, `mapEquiv_trans`, `unitary.mapEquiv_refl`, `toMonoidHom_mapEquiv`, `mapEquiv_refl`
`toUnits` 📖	CompOp	11 math math: `toUnits_injective`, `unitary.toUnits_comp_map`, `unitary.toUnits_injective`, `unitary.val_toUnits_apply`, `LinearIsometryEquiv.toLinearEquiv_smul`, `toAlgEquiv_conjStarAlgAut`, `toRingEquiv_conjStarAlgAut`, `val_toUnits_apply`, `val_inv_toUnits_apply`, `toUnits_comp_map`, `LinearIsometryEquiv.toContinuousLinearEquiv_smul`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_div` 📖	mathematical	—	`Submonoid` `Monoid.toMulOneClass` `MonoidWithZero.toMonoid` `GroupWithZero.toMonoidWithZero` `SetLike.instMembership` `Submonoid.instSetLike` `unitary` `DivInvMonoid.toDiv` `Group.toDivInvMonoid` `instGroupSubtypeMemSubmonoidUnitary` `GroupWithZero.toDivInvMonoid`	—	`div_eq_mul_inv` `coe_inv`
`coe_inv` 📖	mathematical	—	`Submonoid` `Monoid.toMulOneClass` `MonoidWithZero.toMonoid` `GroupWithZero.toMonoidWithZero` `SetLike.instMembership` `Submonoid.instSetLike` `unitary` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `instGroupSubtypeMemSubmonoidUnitary` `GroupWithZero.toDivisionMonoid`	—	`eq_inv_of_mul_eq_one_right` `coe_mul_star_self`
`coe_isStarNormal` 📖	mathematical	—	`IsStarNormal` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `InvolutiveStar.toStar` `StarMul.toInvolutiveStar` `Submonoid` `SetLike.instMembership` `Submonoid.instSetLike` `unitary`	—	`star_comm_self'` `instIsStarNormal`
`coe_map` 📖	mathematical	—	`Submonoid` `Monoid.toMulOneClass` `SetLike.instMembership` `Submonoid.instSetLike` `unitary` `DFunLike.coe` `StarMonoidHom` `Submonoid.toMonoid` `instStarSubtypeMemSubmonoidUnitary` `StarMonoidHom.instFunLike` `map` `InvolutiveStar.toStar` `StarMul.toInvolutiveStar` `MulOne.toMul` `MulOneClass.toMulOne`	—	—
`coe_map_star` 📖	mathematical	—	`Submonoid` `Monoid.toMulOneClass` `SetLike.instMembership` `Submonoid.instSetLike` `unitary` `DFunLike.coe` `StarMonoidHom` `Submonoid.toMonoid` `instStarSubtypeMemSubmonoidUnitary` `StarMonoidHom.instFunLike` `map` `Star.star` `InvolutiveStar.toStar` `StarMul.toInvolutiveStar` `MulOne.toMul` `MulOneClass.toMulOne`	—	—
`coe_mul_star_self` 📖	mathematical	—	`MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `Submonoid` `SetLike.instMembership` `Submonoid.instSetLike` `unitary` `Star.star` `instStarSubtypeMemSubmonoidUnitary` `MulOne.toOne`	—	`mul_star_self_of_mem` `Subtype.prop`
`coe_neg` 📖	mathematical	—	`Submonoid` `Monoid.toMulOneClass` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `SetLike.instMembership` `Submonoid.instSetLike` `unitary` `StarRing.toStarMul` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonUnitalSemiring` `instNegSubtypeMemSubmonoidUnitary` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup`	—	—
`coe_smul` 📖	mathematical	—	`Submonoid` `Monoid.toMulOneClass` `SetLike.instMembership` `Submonoid.instSetLike` `unitary` `instSMulSubtypeMemSubmonoidUnitary` `Submonoid.smul` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MulAction.toSemigroupAction`	—	—
`coe_star` 📖	mathematical	—	`Submonoid` `Monoid.toMulOneClass` `SetLike.instMembership` `Submonoid.instSetLike` `unitary` `Star.star` `instStarSubtypeMemSubmonoidUnitary` `InvolutiveStar.toStar` `StarMul.toInvolutiveStar` `MulOne.toMul` `MulOneClass.toMulOne`	—	—
`coe_star_mul_self` 📖	mathematical	—	`MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `Star.star` `InvolutiveStar.toStar` `StarMul.toInvolutiveStar` `Submonoid` `SetLike.instMembership` `Submonoid.instSetLike` `unitary` `MulOne.toOne`	—	`star_mul_self_of_mem` `Subtype.prop`
`coe_zpow` 📖	mathematical	—	`Submonoid` `Monoid.toMulOneClass` `MonoidWithZero.toMonoid` `GroupWithZero.toMonoidWithZero` `SetLike.instMembership` `Submonoid.instSetLike` `unitary` `DivInvMonoid.toZPow` `Group.toDivInvMonoid` `instGroupSubtypeMemSubmonoidUnitary` `GroupWithZero.toDivInvMonoid`	—	`zpow_natCast` `zpow_negSucc` `coe_inv`
`instIsScalarTowerSubtypeMemSubmonoidUnitary` 📖	mathematical	—	`IsScalarTower` `Submonoid` `Monoid.toMulOneClass` `SetLike.instMembership` `Submonoid.instSetLike` `unitary` `instSMulSubtypeMemSubmonoidUnitary`	—	`smul_assoc` `Submonoid.isScalarTower`
`instIsStarNormal` 📖	mathematical	—	`IsStarNormal` `Submonoid` `Monoid.toMulOneClass` `SetLike.instMembership` `Submonoid.instSetLike` `unitary` `Submonoid.mul` `instStarSubtypeMemSubmonoidUnitary`	—	`star_mul_self` `mul_star_self`
`instSMulCommClassSubtypeMemSubmonoidUnitary` 📖	mathematical	—	`SMulCommClass` `Submonoid` `Monoid.toMulOneClass` `SetLike.instMembership` `Submonoid.instSetLike` `unitary` `instSMulSubtypeMemSubmonoidUnitary`	—	`SMulCommClass.smul_comm` `Submonoid.smulCommClass_left`
`instStarModuleSubtypeMemSubmonoidUnitary` 📖	mathematical	—	`StarModule` `Submonoid` `Monoid.toMulOneClass` `SetLike.instMembership` `Submonoid.instSetLike` `unitary` `instStarSubtypeMemSubmonoidUnitary` `instSMulSubtypeMemSubmonoidUnitary`	—	`StarModule.star_smul`
`inv_mem` 📖	mathematical	`Submonoid` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `SetLike.instMembership` `Submonoid.instSetLike` `unitary`	`InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	—	`star_inv`
`inv_mem_iff` 📖	mathematical	—	`Submonoid` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `SetLike.instMembership` `Submonoid.instSetLike` `unitary` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	—	`inv_mem_iff` `SubgroupClass.toInvMemClass` `Subgroup.instSubgroupClass`
`inv_mul_mem_iff` 📖	mathematical	—	`Submonoid` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `SetLike.instMembership` `Submonoid.instSetLike` `unitary` `MulOne.toMul` `MulOneClass.toMulOne` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `Star.star` `InvolutiveStar.toStar` `StarMul.toInvolutiveStar`	—	`inv_inv` `star_inv` `mul_inv_mem_iff`
`isUnit_coe` 📖	mathematical	—	`IsUnit` `Submonoid` `Monoid.toMulOneClass` `SetLike.instMembership` `Submonoid.instSetLike` `unitary`	—	`Units.isUnit`
`mapEquiv_apply` 📖	mathematical	—	`DFunLike.coe` `StarMulEquiv` `Submonoid` `Monoid.toMulOneClass` `SetLike.instMembership` `Submonoid.instSetLike` `unitary` `Submonoid.mul` `instStarSubtypeMemSubmonoidUnitary` `EquivLike.toFunLike` `StarMulEquiv.instEquivLike` `mapEquiv` `StarMonoidHom` `Submonoid.toMonoid` `StarMonoidHom.instFunLike` `map` `StarMulEquiv.toStarMonoidHom` `InvolutiveStar.toStar` `StarMul.toInvolutiveStar` `MulOne.toMul` `MulOneClass.toMulOne`	—	—
`mapEquiv_refl` 📖	mathematical	—	`mapEquiv` `StarMulEquiv.refl` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `InvolutiveStar.toStar` `StarMul.toInvolutiveStar` `Submonoid` `SetLike.instMembership` `Submonoid.instSetLike` `unitary` `Submonoid.mul` `instStarSubtypeMemSubmonoidUnitary`	—	—
`mapEquiv_symm` 📖	mathematical	—	`mapEquiv` `StarMulEquiv.symm` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `InvolutiveStar.toStar` `StarMul.toInvolutiveStar` `Submonoid` `SetLike.instMembership` `Submonoid.instSetLike` `unitary` `Submonoid.mul` `instStarSubtypeMemSubmonoidUnitary`	—	—
`mapEquiv_symm_apply` 📖	mathematical	—	`DFunLike.coe` `StarMulEquiv` `Submonoid` `Monoid.toMulOneClass` `SetLike.instMembership` `Submonoid.instSetLike` `unitary` `Submonoid.mul` `instStarSubtypeMemSubmonoidUnitary` `EquivLike.toFunLike` `StarMulEquiv.instEquivLike` `StarMulEquiv.symm` `mapEquiv` `StarMonoidHom` `Submonoid.toMonoid` `StarMonoidHom.instFunLike` `map` `StarMulEquiv.toStarMonoidHom` `InvolutiveStar.toStar` `StarMul.toInvolutiveStar` `MulOne.toMul` `MulOneClass.toMulOne`	—	—
`mapEquiv_trans` 📖	mathematical	—	`mapEquiv` `StarMulEquiv.trans` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `InvolutiveStar.toStar` `StarMul.toInvolutiveStar` `Submonoid` `SetLike.instMembership` `Submonoid.instSetLike` `unitary` `Submonoid.mul` `instStarSubtypeMemSubmonoidUnitary`	—	—
`map_coe` 📖	mathematical	—	`DFunLike.coe` `StarMonoidHom` `Submonoid` `Monoid.toMulOneClass` `SetLike.instMembership` `Submonoid.instSetLike` `unitary` `Submonoid.toMonoid` `instStarSubtypeMemSubmonoidUnitary` `StarMonoidHom.instFunLike` `map` `Subtype.map` `InvolutiveStar.toStar` `StarMul.toInvolutiveStar` `MulOne.toMul` `MulOneClass.toMulOne`	—	—
`map_comp` 📖	mathematical	—	`map` `StarMonoidHom.comp` `InvolutiveStar.toStar` `StarMul.toInvolutiveStar` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `Submonoid` `SetLike.instMembership` `Submonoid.instSetLike` `unitary` `Submonoid.toMonoid` `instStarSubtypeMemSubmonoidUnitary`	—	—
`map_id` 📖	mathematical	—	`map` `StarMonoidHom.id` `InvolutiveStar.toStar` `StarMul.toInvolutiveStar` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `Submonoid` `SetLike.instMembership` `Submonoid.instSetLike` `unitary` `Submonoid.toMonoid` `instStarSubtypeMemSubmonoidUnitary`	—	—
`map_injective` 📖	mathematical	`DFunLike.coe` `StarMonoidHom` `InvolutiveStar.toStar` `StarMul.toInvolutiveStar` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `StarMonoidHom.instFunLike`	`Submonoid` `SetLike.instMembership` `Submonoid.instSetLike` `unitary` `Submonoid.toMonoid` `instStarSubtypeMemSubmonoidUnitary` `map`	—	`Subtype.map_injective` `map_mem` `StarMonoidHom.instStarHomClass` `StarMonoidHom.instMonoidHomClass`
`map_mem` 📖	mathematical	`Submonoid` `Monoid.toMulOneClass` `SetLike.instMembership` `Submonoid.instSetLike` `unitary`	`DFunLike.coe`	—	`map_mul` `MonoidHomClass.toMulHomClass` `StarHomClass.map_star` `map_one` `MonoidHomClass.toOneHomClass` `mem_iff`
`mem_iff` 📖	mathematical	—	`Submonoid` `Monoid.toMulOneClass` `SetLike.instMembership` `Submonoid.instSetLike` `unitary` `MulOne.toMul` `MulOneClass.toMulOne` `Star.star` `InvolutiveStar.toStar` `StarMul.toInvolutiveStar` `MulOne.toOne`	—	—
`mem_iff_self_mul_star` 📖	mathematical	—	`Submonoid` `Monoid.toMulOneClass` `CommMonoid.toMonoid` `SetLike.instMembership` `Submonoid.instSetLike` `unitary` `MulOne.toMul` `MulOneClass.toMulOne` `Star.star` `InvolutiveStar.toStar` `StarMul.toInvolutiveStar` `MulOne.toOne`	—	`mem_iff` `mul_comm`
`mem_iff_star_mul_self` 📖	mathematical	—	`Submonoid` `Monoid.toMulOneClass` `CommMonoid.toMonoid` `SetLike.instMembership` `Submonoid.instSetLike` `unitary` `MulOne.toMul` `MulOneClass.toMulOne` `Star.star` `InvolutiveStar.toStar` `StarMul.toInvolutiveStar` `MulOne.toOne`	—	`mem_iff` `mul_comm`
`mul_inv_mem_iff` 📖	mathematical	—	`Submonoid` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `SetLike.instMembership` `Submonoid.instSetLike` `unitary` `MulOne.toMul` `MulOneClass.toMulOne` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `Star.star` `InvolutiveStar.toStar` `StarMul.toInvolutiveStar`	—	`IsUnit.mem_unitary_iff_star_mul_self` `Group.isUnit` `StarMul.star_mul` `star_inv` `mul_assoc` `inv_mul_eq_iff_eq_mul` `mul_one` `mul_inv_eq_iff_eq_mul`
`mul_left_inj` 📖	mathematical	—	`MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `Submonoid` `SetLike.instMembership` `Submonoid.instSetLike` `unitary`	—	`val_toUnits_apply`
`mul_right_inj` 📖	mathematical	—	`MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `Submonoid` `SetLike.instMembership` `Submonoid.instSetLike` `unitary`	—	`val_toUnits_apply`
`mul_star_self` 📖	mathematical	—	`Submonoid` `Monoid.toMulOneClass` `SetLike.instMembership` `Submonoid.instSetLike` `unitary` `Submonoid.mul` `Star.star` `instStarSubtypeMemSubmonoidUnitary` `Submonoid.one`	—	`coe_mul_star_self`
`mul_star_self_of_mem` 📖	mathematical	`Submonoid` `Monoid.toMulOneClass` `SetLike.instMembership` `Submonoid.instSetLike` `unitary`	`MulOne.toMul` `MulOneClass.toMulOne` `Star.star` `InvolutiveStar.toStar` `StarMul.toInvolutiveStar` `MulOne.toOne`	—	—
`smul_mem` 📖	mathematical	`Submonoid` `Monoid.toMulOneClass` `SetLike.instMembership` `Submonoid.instSetLike` `unitary`	`Submonoid.smul` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MulAction.toSemigroupAction`	—	`smul_mem_of_mem` `Subtype.prop`
`smul_mem_of_mem` 📖	mathematical	`Submonoid` `Monoid.toMulOneClass` `SetLike.instMembership` `Submonoid.instSetLike` `unitary`	`SemigroupAction.toSMul` `Monoid.toSemigroup` `MulAction.toSemigroupAction`	—	`StarModule.star_smul` `mul_smul_comm` `smul_mul_assoc` `star_mul_self_of_mem` `smul_smul` `mul_star_self_of_mem` `one_smul`
`spectrum_star_left_conjugate` 📖	mathematical	—	`spectrum` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Star.star` `InvolutiveStar.toStar` `StarMul.toInvolutiveStar` `Submonoid` `Monoid.toMulOneClass` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `SetLike.instMembership` `Submonoid.instSetLike` `unitary`	—	`star_star` `spectrum_star_right_conjugate`
`spectrum_star_right_conjugate` 📖	mathematical	—	`spectrum` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Submonoid` `Monoid.toMulOneClass` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `SetLike.instMembership` `Submonoid.instSetLike` `unitary` `Star.star` `InvolutiveStar.toStar` `StarMul.toInvolutiveStar`	—	`spectrum.units_conjugate`
`star_eq_inv` 📖	mathematical	—	`Star.star` `Submonoid` `Monoid.toMulOneClass` `SetLike.instMembership` `Submonoid.instSetLike` `unitary` `instStarSubtypeMemSubmonoidUnitary` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `instGroupSubtypeMemSubmonoidUnitary`	—	—
`star_eq_inv'` 📖	mathematical	—	`Star.star` `Submonoid` `Monoid.toMulOneClass` `SetLike.instMembership` `Submonoid.instSetLike` `unitary` `instStarSubtypeMemSubmonoidUnitary` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `instGroupSubtypeMemSubmonoidUnitary`	—	—
`star_mem` 📖	mathematical	`Submonoid` `Monoid.toMulOneClass` `SetLike.instMembership` `Submonoid.instSetLike` `unitary`	`Star.star` `InvolutiveStar.toStar` `StarMul.toInvolutiveStar` `MulOne.toMul` `MulOneClass.toMulOne`	—	`star_star` `mul_star_self_of_mem` `star_mul_self_of_mem`
`star_mem_iff` 📖	mathematical	—	`Submonoid` `Monoid.toMulOneClass` `SetLike.instMembership` `Submonoid.instSetLike` `unitary` `Star.star` `InvolutiveStar.toStar` `StarMul.toInvolutiveStar` `MulOne.toMul` `MulOneClass.toMulOne`	—	`star_mem` `star_star`
`star_mul_self` 📖	mathematical	—	`Submonoid` `Monoid.toMulOneClass` `SetLike.instMembership` `Submonoid.instSetLike` `unitary` `Submonoid.mul` `Star.star` `instStarSubtypeMemSubmonoidUnitary` `Submonoid.one`	—	`coe_star_mul_self`
`star_mul_self_of_mem` 📖	mathematical	`Submonoid` `Monoid.toMulOneClass` `SetLike.instMembership` `Submonoid.instSetLike` `unitary`	`MulOne.toMul` `MulOneClass.toMulOne` `Star.star` `InvolutiveStar.toStar` `StarMul.toInvolutiveStar` `MulOne.toOne`	—	—
`toMonoidHom_mapEquiv` 📖	mathematical	—	`StarMulEquiv.toStarMonoidHom` `Submonoid` `Monoid.toMulOneClass` `SetLike.instMembership` `Submonoid.instSetLike` `unitary` `Submonoid.toMonoid` `instStarSubtypeMemSubmonoidUnitary` `mapEquiv` `map` `InvolutiveStar.toStar` `StarMul.toInvolutiveStar` `MulOne.toMul` `MulOneClass.toMulOne`	—	—
`toUnits_comp_map` 📖	mathematical	—	`MonoidHom.comp` `Submonoid` `Monoid.toMulOneClass` `SetLike.instMembership` `Submonoid.instSetLike` `unitary` `Units` `MulOneClass.toMulOne` `Submonoid.toMonoid` `Submonoid.toMulOneClass` `Units.instMulOneClass` `toUnits` `StarMonoidHom.toMonoidHom` `instStarSubtypeMemSubmonoidUnitary` `map` `Units.map` `InvolutiveStar.toStar` `StarMul.toInvolutiveStar` `MulOne.toMul`	—	`MonoidHom.ext` `Units.ext`
`toUnits_injective` 📖	mathematical	—	`Submonoid` `Monoid.toMulOneClass` `SetLike.instMembership` `Submonoid.instSetLike` `unitary` `Units` `DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Submonoid.toMulOneClass` `Units.instMulOneClass` `MonoidHom.instFunLike` `toUnits`	—	`Units.ext_iff`
`val_inv_toUnits_apply` 📖	mathematical	—	`Units.val` `Units` `Units.instInv` `DFunLike.coe` `MonoidHom` `Submonoid` `Monoid.toMulOneClass` `SetLike.instMembership` `Submonoid.instSetLike` `unitary` `MulOneClass.toMulOne` `Submonoid.toMulOneClass` `Units.instMulOneClass` `MonoidHom.instFunLike` `toUnits` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `instGroupSubtypeMemSubmonoidUnitary`	—	—
`val_toUnits_apply` 📖	mathematical	—	`Units.val` `DFunLike.coe` `MonoidHom` `Submonoid` `Monoid.toMulOneClass` `SetLike.instMembership` `Submonoid.instSetLike` `unitary` `Units` `MulOneClass.toMulOne` `Submonoid.toMulOneClass` `Units.instMulOneClass` `MonoidHom.instFunLike` `toUnits`	—	—

Units

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`inv_mul_mem_unitary` 📖	mathematical	—	`Submonoid` `Monoid.toMulOneClass` `SetLike.instMembership` `Submonoid.instSetLike` `unitary` `MulOne.toMul` `MulOneClass.toMulOne` `val` `Units` `instInv` `instMul` `Star.star` `InvolutiveStar.toStar` `StarMul.toInvolutiveStar` `instStarMul`	—	`MonoidHom.instMonoidHomClass` `unitary_eq`
`mul_inv_mem_unitary` 📖	mathematical	—	`Submonoid` `Monoid.toMulOneClass` `SetLike.instMembership` `Submonoid.instSetLike` `unitary` `MulOne.toMul` `MulOneClass.toMulOne` `val` `Units` `instInv` `instMul` `Star.star` `InvolutiveStar.toStar` `StarMul.toInvolutiveStar` `instStarMul`	—	`MonoidHom.instMonoidHomClass` `unitary_eq`
`unitary_eq` 📖	mathematical	—	`unitary` `Units` `instMonoid` `instStarMul` `Submonoid.comap` `instMulOneClass` `Monoid.toMulOneClass` `MonoidHom` `MulOneClass.toMulOne` `MonoidHom.instFunLike` `MonoidHom.instMonoidHomClass` `coeHom`	—	`Submonoid.ext` `MonoidHom.instMonoidHomClass`

(root)

Definitions

Name	Category	Theorems
`unitary` 📖	CompOp	180 math math: `unitary.spectrum.unitary_conjugate`, `Unitary.openPartialHomeomorph_source`, `CStarRing.norm_mul_coe_unitary`, `unitary.star_eq_inv'`, `Unitary.mul_left_inj`, `Unitary.conjStarAlgAut_trans_conjStarAlgAut`, `CStarRing.norm_unitary_smul`, `Unitary.conjStarAlgAut_symm`, `unitary.map_id`, `Unitary.mem_pathComponentOne_iff`, `Unitary.toUnits_injective`, `val_inv_unitarySubgroupUnitsEquiv_symm_apply_coe`, `unitary.inv_mul_mem_iff`, `Unitary.coe_zpow`, `Unitary.conjStarAlgEquiv_unitaryLinearIsometryEquiv`, `selfAdjoint.expUnitaryPathToOne_apply`, `Unitary.continuousOn_argSelfAdjoint`, `Unitary.mapEquiv_symm_apply`, `selfAdjoint.norm_sq_expUnitary_sub_one`, `val_unitarySubgroupUnitsEquiv_symm_apply_coe`, `mem_unitarySubgroup_iff`, `unitary.coe_star_mul_self`, `Unitary.coe_linearIsometryEquiv_apply`, `Unitary.inv_mul_mem_iff`, `unitary.spectrum.unitary_conjugate'`, `Pell.is_pell_solution_iff_mem_unitary`, `unitary.mem_iff_self_mul_star`, `unitary.coe_div`, `Unitary.linearIsometryEquiv_coe_apply`, `LinearIsometryEquiv.trans_smul`, `unitary.coe_zpow`, `unitary.map_comp`, `unitary.mapEquiv_trans`, `QuadraticAlgebra.norm_eq_one_iff_mem_unitary`, `Zsqrtd.mker_norm_eq_unitary`, `Unitary.spectrum_star_left_conjugate`, `Unitary.openPartialHomeomorph_symm_apply`, `Units.mul_inv_mem_unitary`, `Pell.Solution₁.coe_mk`, `instIsTopologicalGroupSubtypeMemSubmonoidUnitaryOfContinuousMulOfContinuousStar`, `unitary.mem_iff`, `Unitary.mem_iff_self_mul_star`, `unitary.coe_smul`, `unitarySubgroupUnitsEquiv_apply_coe`, `LinearIsometryEquiv.smul_apply`, `Unitary.map_coe`, `unitary.linearIsometryEquiv_coe_symm_apply`, `unitary.toUnits_comp_map`, `unitary.norm_sub_eq`, `Unitary.coe_symm_linearIsometryEquiv_apply`, `selfAdjoint.expUnitary_zero`, `unitary.mem_iff_star_mul_self`, `Unitary.instLocPathConnectedSpace`, `Unitary.coe_mul_star_self`, `pinGroup.mem_unitary`, `Unitary.mul_star_self`, `Unitary.spectrum_star_right_conjugate`, `selfAdjoint.continuous_expUnitary`, `Unitary.conjStarAlgAut_ext_iff'`, `selfAdjoint.unitarySelfAddISMul_coe`, `QuadraticAlgebra.mem_unitary`, `unitary.mul_left_inj`, `LinearIsometryEquiv.conjStarAlgEquiv_ext_iff`, `Unitary.map_comp`, `Unitary.mul_right_inj`, `Unitary.mapEquiv_apply`, `unitary.toUnits_injective`, `Units.unitary_eq`, `Pell.isPell_iff_mem_unitary`, `Unitary.coe_smul`, `CStarAlgebra.norm_smul_two_inv_smul_add_four_unitary`, `Matrix.IsHermitian.cfcAux_apply`, `IsUnit.mem_unitary_of_star_mul_self`, `Unitary.linearIsometryEquiv_coe_symm_apply`, `Unitary.star_mul_self`, `unitary.spectrum_subset_circle`, `unitary.val_toUnits_apply`, `Unitary.mul_inv_mem_iff`, `Unitary.instIsStarNormal`, `Unitary.conjStarAlgAut_apply`, `LinearIsometryEquiv.toLinearEquiv_smul`, `unitary.mapEquiv_symm`, `Unitary.mem_iff_star_mul_self`, `Unitary.toAlgEquiv_conjStarAlgAut`, `pinGroup.units_mem_iff`, `selfAdjoint.realPart_unitarySelfAddISMul`, `Unitary.openPartialHomeomorph_target`, `Unitary.inv_mem_iff`, `Matrix.det_of_mem_unitary`, `unitary.coe_mul_star_self`, `Unitary.coe_isStarNormal`, `Unitary.conjStarAlgAut_symm_apply`, `selfAdjoint.star_coe_unitarySelfAddISMul`, `Unitary.toRingEquiv_conjStarAlgAut`, `Unitary.val_toUnits_apply`, `unitary.coe_inv`, `Matrix.IsHermitian.spectral_theorem`, `unitary.coe_map`, `Unitary.coe_div`, `QuadraticAlgebra.mker_norm_eq_unitary`, `Unitary.val_inv_toUnits_apply`, `Unitary.norm_map`, `Unitary.toUnits_comp_map`, `Unitary.coe_map_star`, `unitary.norm_map`, `Unitary.instSMulCommClassSubtypeMemSubmonoidUnitary`, `unitary.coe_map_star`, `Commute.expUnitary_add`, `Unitary.isPathConnected_ball`, `unitarySubgroup_toSubmonoid`, `Unitary.map_injective`, `Unitary.mapEquiv_symm`, `instContinuousStarSubtypeMemSubmonoidUnitary`, `Unitary.conjStarAlgAut_mul_apply`, `cfc_unitary_iff`, `unitary.toMonoidHom_mapEquiv`, `Unitary.map_id`, `IsStarProjection.two_mul_sub_one_mem_unitary`, `Unitary.mapEquiv_trans`, `pinGroup.mem_iff`, `LinearIsometryEquiv.smul_trans`, `Unitary.inner_map_map`, `Unitary.norm_sub_eq`, `unitary_iff_isStarNormal_and_spectrum_subset_unitary`, `unitary.coe_star`, `Unitary.coe_map`, `unitary.mul_inv_mem_iff`, `unitary.mapEquiv_refl`, `LinearIsometryEquiv.symm_units_smul`, `Unitary.mem_iff`, `Unitary.instIsScalarTowerSubtypeMemSubmonoidUnitary`, `LinearIsometryEquiv.symm_smul_apply`, `IsSelfAdjoint.self_add_I_smul_cfcSqrt_sub_sq_mem_unitary`, `Unitary.coe_neg`, `Matrix.IsHermitian.star_mul_self_mul_eq_diagonal`, `Unitary.star_eq_inv`, `CStarRing.norm_coe_unitary_mul`, `instContinuousInvSubtypeMemSubmonoidUnitaryOfContinuousStar`, `Unitary.conjStarAlgAut_symm_unitaryLinearIsometryEquiv`, `unitary.isPathConnected_ball`, `Zsqrtd.norm_eq_one_iff_mem_unitary`, `IsUnit.mem_unitary_of_mul_star_self`, `Unitary.coe_star_mul_self`, `unitary.map_injective`, `Unitary.instStarModuleSubtypeMemSubmonoidUnitary`, `Unitary.toMonoidHom_mapEquiv`, `IsUnit.mem_unitary_iff_mul_star_self`, `Unitary.star_mem_iff`, `Unitary.openPartialHomeomorph_apply`, `Matrix.IsHermitian.conjStarAlgAut_star_eigenvectorUnitary`, `Unitary.argSelfAdjoint_coe`, `unitary.mul_star_self`, `unitary.star_mem_iff`, `CStarAlgebra.exists_sum_four_unitary`, `Unitary.coe_star`, `NormedSpace.exp_mem_unitary_of_mem_skewAdjoint`, `Unitary.conjStarAlgAut_star_apply`, `unitary.coe_neg`, `LinearIsometryEquiv.toContinuousLinearEquiv_smul`, `unitary.star_eq_inv`, `unitary.mem_pathComponentOne_iff`, `Unitary.mapEquiv_refl`, `CStarRing.norm_coe_unitary`, `Unitary.star_eq_inv'`, `CStarAlgebra.span_unitary`, `IsUnit.mem_unitary_iff_star_mul_self`, `Unitary.conjStarAlgAut_ext_iff`, `Unitary.spectrum_subset_circle`, `Unitary.isUnit_coe`, `unitary.mul_right_inj`, `Commute.expUnitary`, `unitary.star_mul_self`, `Units.inv_mul_mem_unitary`, `Unitary.coe_inv`, `selfAdjoint.expUnitary_coe`, `isClosed_unitary`, `unitary.inner_map_map`, `selfAdjoint.joined_one_expUnitary`, `unitary.continuousOn_argSelfAdjoint`, `unitary.linearIsometryEquiv_coe_apply`
`unitarySubgroup` 📖	CompOp	5 math math: `val_inv_unitarySubgroupUnitsEquiv_symm_apply_coe`, `val_unitarySubgroupUnitsEquiv_symm_apply_coe`, `mem_unitarySubgroup_iff`, `unitarySubgroupUnitsEquiv_apply_coe`, `unitarySubgroup_toSubmonoid`
`unitarySubgroupUnitsEquiv` 📖	CompOp	3 math math: `val_inv_unitarySubgroupUnitsEquiv_symm_apply_coe`, `val_unitarySubgroupUnitsEquiv_symm_apply_coe`, `unitarySubgroupUnitsEquiv_apply_coe`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isStarNormal_of_mem_unitary` 📖	mathematical	`Submonoid` `Monoid.toMulOneClass` `SetLike.instMembership` `Submonoid.instSetLike` `unitary`	`IsStarNormal` `MulOne.toMul` `MulOneClass.toMulOne` `InvolutiveStar.toStar` `StarMul.toInvolutiveStar`	—	`Unitary.coe_isStarNormal`
`mem_unitarySubgroup_iff` 📖	mathematical	—	`Subgroup` `SetLike.instMembership` `Subgroup.instSetLike` `unitarySubgroup` `Submonoid` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Submonoid.instSetLike` `unitary`	—	—
`unitarySubgroupUnitsEquiv_apply_coe` 📖	mathematical	—	`Submonoid` `Monoid.toMulOneClass` `SetLike.instMembership` `Submonoid.instSetLike` `unitary` `DFunLike.coe` `MulEquiv` `Units` `Subgroup` `Units.instGroup` `Subgroup.instSetLike` `unitarySubgroup` `Units.instStarMul` `Subgroup.mul` `Submonoid.mul` `EquivLike.toFunLike` `MulEquiv.instEquivLike` `unitarySubgroupUnitsEquiv` `Units.val`	—	—
`unitarySubgroup_toSubmonoid` 📖	mathematical	—	`Subgroup.toSubmonoid` `unitarySubgroup` `unitary` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid`	—	—
`val_inv_unitarySubgroupUnitsEquiv_symm_apply_coe` 📖	mathematical	—	`Units.val` `Units` `Units.instInv` `Subgroup` `Units.instGroup` `SetLike.instMembership` `Subgroup.instSetLike` `unitarySubgroup` `Units.instStarMul` `DFunLike.coe` `MulEquiv` `Submonoid` `Monoid.toMulOneClass` `Submonoid.instSetLike` `unitary` `Submonoid.mul` `Subgroup.mul` `EquivLike.toFunLike` `MulEquiv.instEquivLike` `MulEquiv.symm` `unitarySubgroupUnitsEquiv` `Star.star` `InvolutiveStar.toStar` `StarMul.toInvolutiveStar` `MulOne.toMul` `MulOneClass.toMulOne`	—	—
`val_unitarySubgroupUnitsEquiv_symm_apply_coe` 📖	mathematical	—	`Units.val` `Units` `Subgroup` `Units.instGroup` `SetLike.instMembership` `Subgroup.instSetLike` `unitarySubgroup` `Units.instStarMul` `DFunLike.coe` `MulEquiv` `Submonoid` `Monoid.toMulOneClass` `Submonoid.instSetLike` `unitary` `Submonoid.mul` `Subgroup.mul` `EquivLike.toFunLike` `MulEquiv.instEquivLike` `MulEquiv.symm` `unitarySubgroupUnitsEquiv`	—	—

unitary

Definitions

Name	Category	Theorems
`map` 📖	CompOp	—
`mapEquiv` 📖	CompOp	—
`toUnits` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_div` 📖	mathematical	—	`Submonoid` `Monoid.toMulOneClass` `MonoidWithZero.toMonoid` `GroupWithZero.toMonoidWithZero` `SetLike.instMembership` `Submonoid.instSetLike` `unitary` `DivInvMonoid.toDiv` `Group.toDivInvMonoid` `Unitary.instGroupSubtypeMemSubmonoidUnitary` `GroupWithZero.toDivInvMonoid`	—	`Unitary.coe_div`
`coe_inv` 📖	mathematical	—	`Submonoid` `Monoid.toMulOneClass` `MonoidWithZero.toMonoid` `GroupWithZero.toMonoidWithZero` `SetLike.instMembership` `Submonoid.instSetLike` `unitary` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `Unitary.instGroupSubtypeMemSubmonoidUnitary` `GroupWithZero.toDivisionMonoid`	—	`Unitary.coe_inv`
`coe_map` 📖	mathematical	—	`Submonoid` `Monoid.toMulOneClass` `SetLike.instMembership` `Submonoid.instSetLike` `unitary` `DFunLike.coe` `StarMonoidHom` `Submonoid.toMonoid` `Unitary.instStarSubtypeMemSubmonoidUnitary` `StarMonoidHom.instFunLike` `Unitary.map` `InvolutiveStar.toStar` `StarMul.toInvolutiveStar` `MulOne.toMul` `MulOneClass.toMulOne`	—	`Unitary.coe_map`
`coe_map_star` 📖	mathematical	—	`Submonoid` `Monoid.toMulOneClass` `SetLike.instMembership` `Submonoid.instSetLike` `unitary` `DFunLike.coe` `StarMonoidHom` `Submonoid.toMonoid` `Unitary.instStarSubtypeMemSubmonoidUnitary` `StarMonoidHom.instFunLike` `Unitary.map` `Star.star` `InvolutiveStar.toStar` `StarMul.toInvolutiveStar` `MulOne.toMul` `MulOneClass.toMulOne`	—	`Unitary.coe_map_star`
`coe_mul_star_self` 📖	mathematical	—	`MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `Submonoid` `SetLike.instMembership` `Submonoid.instSetLike` `unitary` `Star.star` `Unitary.instStarSubtypeMemSubmonoidUnitary` `MulOne.toOne`	—	`Unitary.coe_mul_star_self`
`coe_neg` 📖	mathematical	—	`Submonoid` `Monoid.toMulOneClass` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `SetLike.instMembership` `Submonoid.instSetLike` `unitary` `StarRing.toStarMul` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonUnitalSemiring` `Unitary.instNegSubtypeMemSubmonoidUnitary` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup`	—	`Unitary.coe_neg`
`coe_smul` 📖	mathematical	—	`Submonoid` `Monoid.toMulOneClass` `SetLike.instMembership` `Submonoid.instSetLike` `unitary` `Unitary.instSMulSubtypeMemSubmonoidUnitary` `Submonoid.smul` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MulAction.toSemigroupAction`	—	`Unitary.coe_smul`
`coe_star` 📖	mathematical	—	`Submonoid` `Monoid.toMulOneClass` `SetLike.instMembership` `Submonoid.instSetLike` `unitary` `Star.star` `Unitary.instStarSubtypeMemSubmonoidUnitary` `InvolutiveStar.toStar` `StarMul.toInvolutiveStar` `MulOne.toMul` `MulOneClass.toMulOne`	—	`Unitary.coe_star`
`coe_star_mul_self` 📖	mathematical	—	`MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `Star.star` `InvolutiveStar.toStar` `StarMul.toInvolutiveStar` `Submonoid` `SetLike.instMembership` `Submonoid.instSetLike` `unitary` `MulOne.toOne`	—	`Unitary.coe_star_mul_self`
`coe_zpow` 📖	mathematical	—	`Submonoid` `Monoid.toMulOneClass` `MonoidWithZero.toMonoid` `GroupWithZero.toMonoidWithZero` `SetLike.instMembership` `Submonoid.instSetLike` `unitary` `DivInvMonoid.toZPow` `Group.toDivInvMonoid` `Unitary.instGroupSubtypeMemSubmonoidUnitary` `GroupWithZero.toDivInvMonoid`	—	`Unitary.coe_zpow`
`inv_mem` 📖	mathematical	`Submonoid` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `SetLike.instMembership` `Submonoid.instSetLike` `unitary`	`InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	—	`Unitary.inv_mem`
`inv_mul_mem_iff` 📖	mathematical	—	`Submonoid` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `SetLike.instMembership` `Submonoid.instSetLike` `unitary` `MulOne.toMul` `MulOneClass.toMulOne` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `Star.star` `InvolutiveStar.toStar` `StarMul.toInvolutiveStar`	—	`Unitary.inv_mul_mem_iff`
`mapEquiv_refl` 📖	mathematical	—	`Unitary.mapEquiv` `StarMulEquiv.refl` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `InvolutiveStar.toStar` `StarMul.toInvolutiveStar` `Submonoid` `SetLike.instMembership` `Submonoid.instSetLike` `unitary` `Submonoid.mul` `Unitary.instStarSubtypeMemSubmonoidUnitary`	—	`Unitary.mapEquiv_refl`
`mapEquiv_symm` 📖	mathematical	—	`Unitary.mapEquiv` `StarMulEquiv.symm` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `InvolutiveStar.toStar` `StarMul.toInvolutiveStar` `Submonoid` `SetLike.instMembership` `Submonoid.instSetLike` `unitary` `Submonoid.mul` `Unitary.instStarSubtypeMemSubmonoidUnitary`	—	`Unitary.mapEquiv_symm`
`mapEquiv_trans` 📖	mathematical	—	`Unitary.mapEquiv` `StarMulEquiv.trans` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `InvolutiveStar.toStar` `StarMul.toInvolutiveStar` `Submonoid` `SetLike.instMembership` `Submonoid.instSetLike` `unitary` `Submonoid.mul` `Unitary.instStarSubtypeMemSubmonoidUnitary`	—	`Unitary.mapEquiv_trans`
`map_comp` 📖	mathematical	—	`Unitary.map` `StarMonoidHom.comp` `InvolutiveStar.toStar` `StarMul.toInvolutiveStar` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `Submonoid` `SetLike.instMembership` `Submonoid.instSetLike` `unitary` `Submonoid.toMonoid` `Unitary.instStarSubtypeMemSubmonoidUnitary`	—	`Unitary.map_comp`
`map_id` 📖	mathematical	—	`Unitary.map` `StarMonoidHom.id` `InvolutiveStar.toStar` `StarMul.toInvolutiveStar` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `Submonoid` `SetLike.instMembership` `Submonoid.instSetLike` `unitary` `Submonoid.toMonoid` `Unitary.instStarSubtypeMemSubmonoidUnitary`	—	`Unitary.map_id`
`map_injective` 📖	mathematical	`DFunLike.coe` `StarMonoidHom` `InvolutiveStar.toStar` `StarMul.toInvolutiveStar` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `StarMonoidHom.instFunLike`	`Submonoid` `SetLike.instMembership` `Submonoid.instSetLike` `unitary` `Submonoid.toMonoid` `Unitary.instStarSubtypeMemSubmonoidUnitary` `Unitary.map`	—	`Unitary.map_injective`
`map_mem` 📖	mathematical	`Submonoid` `Monoid.toMulOneClass` `SetLike.instMembership` `Submonoid.instSetLike` `unitary`	`DFunLike.coe`	—	`Unitary.map_mem`
`mem_iff` 📖	mathematical	—	`Submonoid` `Monoid.toMulOneClass` `SetLike.instMembership` `Submonoid.instSetLike` `unitary` `MulOne.toMul` `MulOneClass.toMulOne` `Star.star` `InvolutiveStar.toStar` `StarMul.toInvolutiveStar` `MulOne.toOne`	—	`Unitary.mem_iff`
`mem_iff_self_mul_star` 📖	mathematical	—	`Submonoid` `Monoid.toMulOneClass` `CommMonoid.toMonoid` `SetLike.instMembership` `Submonoid.instSetLike` `unitary` `MulOne.toMul` `MulOneClass.toMulOne` `Star.star` `InvolutiveStar.toStar` `StarMul.toInvolutiveStar` `MulOne.toOne`	—	`Unitary.mem_iff_self_mul_star`
`mem_iff_star_mul_self` 📖	mathematical	—	`Submonoid` `Monoid.toMulOneClass` `CommMonoid.toMonoid` `SetLike.instMembership` `Submonoid.instSetLike` `unitary` `MulOne.toMul` `MulOneClass.toMulOne` `Star.star` `InvolutiveStar.toStar` `StarMul.toInvolutiveStar` `MulOne.toOne`	—	`Unitary.mem_iff_star_mul_self`
`mul_inv_mem_iff` 📖	mathematical	—	`Submonoid` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `SetLike.instMembership` `Submonoid.instSetLike` `unitary` `MulOne.toMul` `MulOneClass.toMulOne` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `Star.star` `InvolutiveStar.toStar` `StarMul.toInvolutiveStar`	—	`Unitary.mul_inv_mem_iff`
`mul_left_inj` 📖	mathematical	—	`MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `Submonoid` `SetLike.instMembership` `Submonoid.instSetLike` `unitary`	—	—
`mul_right_inj` 📖	mathematical	—	`MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `Submonoid` `SetLike.instMembership` `Submonoid.instSetLike` `unitary`	—	—
`mul_star_self` 📖	mathematical	—	`Submonoid` `Monoid.toMulOneClass` `SetLike.instMembership` `Submonoid.instSetLike` `unitary` `Submonoid.mul` `Star.star` `Unitary.instStarSubtypeMemSubmonoidUnitary` `Submonoid.one`	—	`Unitary.mul_star_self`
`mul_star_self_of_mem` 📖	mathematical	`Submonoid` `Monoid.toMulOneClass` `SetLike.instMembership` `Submonoid.instSetLike` `unitary`	`MulOne.toMul` `MulOneClass.toMulOne` `Star.star` `InvolutiveStar.toStar` `StarMul.toInvolutiveStar` `MulOne.toOne`	—	`Unitary.mul_star_self_of_mem`
`smul_mem` 📖	mathematical	`Submonoid` `Monoid.toMulOneClass` `SetLike.instMembership` `Submonoid.instSetLike` `unitary`	`Submonoid.smul` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MulAction.toSemigroupAction`	—	`Unitary.smul_mem`
`smul_mem_of_mem` 📖	mathematical	`Submonoid` `Monoid.toMulOneClass` `SetLike.instMembership` `Submonoid.instSetLike` `unitary`	`SemigroupAction.toSMul` `Monoid.toSemigroup` `MulAction.toSemigroupAction`	—	`Unitary.smul_mem_of_mem`
`star_eq_inv` 📖	mathematical	—	`Star.star` `Submonoid` `Monoid.toMulOneClass` `SetLike.instMembership` `Submonoid.instSetLike` `unitary` `Unitary.instStarSubtypeMemSubmonoidUnitary` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `Unitary.instGroupSubtypeMemSubmonoidUnitary`	—	`Unitary.star_eq_inv`
`star_eq_inv'` 📖	mathematical	—	`Star.star` `Submonoid` `Monoid.toMulOneClass` `SetLike.instMembership` `Submonoid.instSetLike` `unitary` `Unitary.instStarSubtypeMemSubmonoidUnitary` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `Unitary.instGroupSubtypeMemSubmonoidUnitary`	—	`Unitary.star_eq_inv'`
`star_mem` 📖	mathematical	`Submonoid` `Monoid.toMulOneClass` `SetLike.instMembership` `Submonoid.instSetLike` `unitary`	`Star.star` `InvolutiveStar.toStar` `StarMul.toInvolutiveStar` `MulOne.toMul` `MulOneClass.toMulOne`	—	`Unitary.star_mem`
`star_mem_iff` 📖	mathematical	—	`Submonoid` `Monoid.toMulOneClass` `SetLike.instMembership` `Submonoid.instSetLike` `unitary` `Star.star` `InvolutiveStar.toStar` `StarMul.toInvolutiveStar` `MulOne.toMul` `MulOneClass.toMulOne`	—	`Unitary.star_mem_iff`
`star_mul_self` 📖	mathematical	—	`Submonoid` `Monoid.toMulOneClass` `SetLike.instMembership` `Submonoid.instSetLike` `unitary` `Submonoid.mul` `Star.star` `Unitary.instStarSubtypeMemSubmonoidUnitary` `Submonoid.one`	—	`Unitary.star_mul_self`
`star_mul_self_of_mem` 📖	mathematical	`Submonoid` `Monoid.toMulOneClass` `SetLike.instMembership` `Submonoid.instSetLike` `unitary`	`MulOne.toMul` `MulOneClass.toMulOne` `Star.star` `InvolutiveStar.toStar` `StarMul.toInvolutiveStar` `MulOne.toOne`	—	`Unitary.star_mul_self_of_mem`
`toMonoidHom_mapEquiv` 📖	mathematical	—	`StarMulEquiv.toStarMonoidHom` `Submonoid` `Monoid.toMulOneClass` `SetLike.instMembership` `Submonoid.instSetLike` `unitary` `Submonoid.toMonoid` `Unitary.instStarSubtypeMemSubmonoidUnitary` `Unitary.mapEquiv` `Unitary.map` `InvolutiveStar.toStar` `StarMul.toInvolutiveStar` `MulOne.toMul` `MulOneClass.toMulOne`	—	`Unitary.toMonoidHom_mapEquiv`
`toUnits_comp_map` 📖	mathematical	—	`MonoidHom.comp` `Submonoid` `Monoid.toMulOneClass` `SetLike.instMembership` `Submonoid.instSetLike` `unitary` `Units` `MulOneClass.toMulOne` `Submonoid.toMonoid` `Submonoid.toMulOneClass` `Units.instMulOneClass` `Unitary.toUnits` `StarMonoidHom.toMonoidHom` `Unitary.instStarSubtypeMemSubmonoidUnitary` `Unitary.map` `Units.map` `InvolutiveStar.toStar` `StarMul.toInvolutiveStar` `MulOne.toMul`	—	`Unitary.toUnits_comp_map`
`toUnits_injective` 📖	mathematical	—	`Submonoid` `Monoid.toMulOneClass` `SetLike.instMembership` `Submonoid.instSetLike` `unitary` `Units` `DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Submonoid.toMulOneClass` `Units.instMulOneClass` `MonoidHom.instFunLike` `Unitary.toUnits`	—	`Unitary.toUnits_injective`
`val_toUnits_apply` 📖	mathematical	—	`Units.val` `DFunLike.coe` `MonoidHom` `Submonoid` `Monoid.toMulOneClass` `SetLike.instMembership` `Submonoid.instSetLike` `unitary` `Units` `MulOneClass.toMulOne` `Submonoid.toMulOneClass` `Units.instMulOneClass` `MonoidHom.instFunLike` `Unitary.toUnits`	—	`Unitary.val_toUnits_apply`

unitary.spectrum

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`unitary_conjugate` 📖	mathematical	—	`spectrum` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Submonoid` `Monoid.toMulOneClass` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `SetLike.instMembership` `Submonoid.instSetLike` `unitary` `Star.star` `InvolutiveStar.toStar` `StarMul.toInvolutiveStar`	—	`Unitary.spectrum_star_right_conjugate`
`unitary_conjugate'` 📖	mathematical	—	`spectrum` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Star.star` `InvolutiveStar.toStar` `StarMul.toInvolutiveStar` `Submonoid` `Monoid.toMulOneClass` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `SetLike.instMembership` `Submonoid.instSetLike` `unitary`	—	`Unitary.spectrum_star_left_conjugate`

---

← Back to Index