Theorems · Theorem · functional analysis

CStarAlgebra.star_right_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_right_conjugate_le_norm_smul._auto_1 →
    a * b * star a ≤ ‖b‖ • (a * star a)

Defined in: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
Cited by: 1 results in Mathlib
Foundations: Depth 319 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.

Cites9

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
Norm.normstatement and proof · cited by 5,413
Star.starstatement and proof · cited by 1,082
StarOrderedRingstatement and proof · cited by 587
IsSelfAdjointstatement and proof · cited by 545
NonUnitalCStarAlgebrastatement and proof · cited by 149
star_starproof · cited by 135
CStarAlgebra.star_left_conjugate_le_norm_smulproof · cited by 1

Cited by1

Results whose statement or proof uses this declaration.

CStarModule.inner_mul_inner_swap_leproof · cited by 1