Theorems · Theorem · functional analysis

CStarAlgebra.star_left_conjugate_le_norm_smul

∀ {A : Type u_1} [inst : NonUnitalCStarAlgebra A] [inst_1 : PartialOrder A] [StarOrderedRing A] {a b : A},
  autoParam (IsSelfAdjoint b) CStarAlgebra.star_left_conjugate_le_norm_smul._auto_1 →
    star a * b * a ≤ ‖b‖ • (star a * a)

Defined in: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
Cited by: 1 results in Mathlib
Foundations: Depth 318 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: NonUnitalCStarAlgebra PartialOrder StarOrderedRing

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites26

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Realstatement · cited by 25,697
PartialOrderstatement and proof · cited by 6,410
Complexproof · cited by 5,565
Norm.normstatement and proof · cited by 5,413
mul_oneproof · cited by 3,885
Star.starstatement and proof · cited by 1,082
StarOrderedRingstatement and proof · cited by 587
IsSelfAdjointstatement and proof · cited by 545
Unitizationproof · cited by 220
NonUnitalCStarAlgebrastatement and proof · cited by 149
Algebra.algebraMap_eq_smul_oneproof · cited by 119
Unitization.inrproof · cited by 109

Cited by1

Results whose statement or proof uses this declaration.

CStarAlgebra.star_right_conjugate_le_norm_smulproof · cited by 1