Theorems · Theorem · linear algebra
isStarNormal_iff_commute_realPart_imaginaryPart
∀ {A : Type u_1} [inst : NonUnitalNonAssocRing A] [inst_1 : StarRing A] [inst_2 : Module ℂ A] [IsScalarTower ℂ A A]
[SMulCommClass ℂ A A] [inst_5 : StarModule ℂ A] {x : A}, IsStarNormal x ↔ Commute ↑(realPart x) ↑(imaginaryPart x)An element in a non-unital star ℂ-algebra is normal if and only if its real and imaginary
parts commute.
- Defined in
- Mathlib.LinearAlgebra.Complex.Module
- Cited by
- 1 results in Mathlib
- Foundations
- Depth 116 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites27
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coestatement and proof · cited by 62,936
- Realstatement · cited by 25,697
- Modulestatement and proof · cited by 20,661
- RingHom.idstatement · cited by 18,349
- LinearMapstatement · cited by 10,215
- Complexstatement and proof · cited by 5,565
- IsScalarTowerstatement and proof · cited by 3,896
- AddSubgroupstatement · cited by 3,232
- SMulCommClassstatement and proof · cited by 1,927
- StarRingstatement and proof · cited by 1,686
- Star.starproof · cited by 1,082
- Complex.Iproof · cited by 866
Cited by1
Results whose statement or proof uses this declaration.
- Commute.realPart_imaginaryPartproof · cited by 1