Theorems · Theorem · ring theory
IsStarNormal.star_comm_self
∀ {R : Type u_1} {inst : Mul R} {inst_1 : Star R} {x : R} [self : IsStarNormal x], Commute (star x) xA normal element of a star monoid commutes with its adjoint.
- Defined in
- Mathlib.Algebra.Star.SelfAdjoint
- Cited by
- 8 results in Mathlib
- Foundations
- Depth 6 from the axioms · uses no axioms
- Assumes
- IsStarNormal
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites4
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Star.starstatement · cited by 1,082
- Commutestatement · cited by 639
- Starstatement and proof · cited by 496
- IsStarNormalstatement and proof · cited by 117
Cited by8
Results whose statement or proof uses this declaration.
- star_comm_self'proof · cited by 3
- Quaternion.star_mul_selfproof · cited by 2
- cfc_unitary_iffproof · cited by 2
- commute_unitary_star_selfproof · cited by 1
- isStarNormal_iff_forall_exp_mul_exp_mem_unitaryproof · cited by 0
- mem_unitary_iff_isStarNormal_and_realPart_sq_add_imaginaryPart_sq_eq_oneproof · cited by 0
- CFC.commute_abs_selfproof · cited by 0
- CFC.abs_mul_selfproof · cited by 0