Structures · Algebra
IsStarNormal
An element of a star monoid is normal if it commutes with its adjoint.
- Defined in
- Mathlib.Algebra.Star.SelfAdjoint
- Shape
- One type argument · adds star_comm_self
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances4
- Quaternion
- Unitization
- QuaternionAlgebra
- Subtype
How is a type an instance?
Loading the hierarchy index…
Assumed by36
- IsStarNormal.star_comm_self
- star_comm_self'
- continuousFunctionalCalculus
- star_mul_self_eq_realPart_sq_add_imaginaryPart_sq
- Commute.realPart_imaginaryPart
- Commute.isStarNormal_add
- continuousFunctionalCalculus_map_id
- IsStarNormal.one_sub
- NonUnitalStarAlgebra.commute_of_mem_adjoin_self
- StarAlgebra.elemental.instCommCStarAlgebraSubtypeMemStarSubalgebraComplexOfIsStarNormal
- mem_unitary_of_spectrum_subset_unitary
- IsStarNormal.map
- StarAlgebra.elemental.instCommSemiringSubtypeMemStarSubalgebraOfT2SpaceOfIsStarNormal
- IsStarNormal.val_inv
- StarAlgebra.elemental.characterSpaceHomeo
- inr_comp_cfcₙHom_eq_cfcₙAux
- StarAlgebra.isMulCommutative_adjoin_singleton
- Unitization.instIsStarNormal
- cfcHom_eq_of_isStarNormal
- instCommCStarAlgebraSubtypeMemStarSubalgebraComplexElementalOfIsStarNormal
- IsStarNormal.neg
- instNonUnitalCommCStarAlgebraSubtypeMemNonUnitalStarSubalgebraComplexElementalOfIsStarNormal
- IsStarNormal.spectralRadius_eq_nnnorm
- Commute.isStarNormal_sub
- StarAlgebra.elemental.instNormedCommRingSubtypeMemStarSubalgebraOfIsStarNormal
- NonUnitalStarAlgebra.isMulCommutative_adjoin_singleton
- StarAlgebra.elemental.instCommRingSubtypeMemStarSubalgebraOfT2SpaceOfIsStarNormal
- StarAlgebra.elemental.bijective_characterSpaceToSpectrum
- StarAlgebra.adjoinCommSemiringOfIsStarNormal
- IsStarNormal.star
- StarAlgebra.adjoinCommRingOfIsStarNormal
- IsStarNormal.one_add
- IsStarNormal.smul
- NonUnitalStarAlgebra.elemental.instNonUnitalCommSemiringSubtypeMemNonUnitalStarSubalgebraOfT2SpaceOfIsStarNormal
- NonUnitalStarAlgebra.elemental.instNonUnitalCommRingSubtypeMemNonUnitalStarSubalgebraOfT2SpaceOfIsStarNormal
- QuasispectrumRestricts.isSelfAdjoint
Ancestors0
No ancestors.