Theorems · Inductive type · ring theory
IsStarNormal
{R : Type u_1} → [Mul R] → [Star R] → R → PropAn element of a star monoid is normal if it commutes with its adjoint.
- Defined in
- Mathlib.Algebra.Star.SelfAdjoint
- Cited by
- 117 results in Mathlib
- Foundations
- Depth 1 from the axioms, rests on 3 definitions · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites1
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Starstatement · cited by 496
Cited by121
Results whose statement or proof uses this declaration.
- IsSelfAdjoint.spectrumRestrictsstatement and proof · cited by 13
- IsStarNormal.star_comm_selfstatement and proof · cited by 8
- IsSelfAdjoint.isStarNormalstatement · cited by 8
- isStarNormal_iffstatement and proof · cited by 6
- IsSelfAdjoint.quasispectrumRestrictsstatement and proof · cited by 6
- cfc_re_idstatement and proof · cited by 4
- cfc_real_eq_complexstatement and proof · cited by 4
- cfcₙ_re_idstatement and proof · cited by 4
- Unitary.argSelfAdjoint_coestatement · cited by 4
- cfc_im_idstatement and proof · cited by 3
- star_comm_self'statement and proof · cited by 3
- IsStarNormal.norm_add_eq_maxstatement and proof · cited by 3