Theorems · Theorem · functional analysis

CStarModule.inner_self_nonneg

∀ {A : Type u_1} {E : Type u_2} {inst : NonUnitalSemiring A} {inst_1 : StarRing A} {inst_2 : Module ℂ A}
  {inst_3 : AddCommGroup E} {inst_4 : Module ℂ E} {inst_5 : PartialOrder A} {inst_6 : SMul A E} {inst_7 : Norm A}
  {inst_8 : Norm E} [self : CStarModule A E] {x : E}, 0 ≤ inner A x x

Defined in: Mathlib.Analysis.CStarAlgebra.Module.Defs
Cited by: 3 results in Mathlib
Foundations: Depth 106 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: CStarModule

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.

Modulestatement and proof · cited by 20,661
AddCommGroupstatement and proof · cited by 12,871
PartialOrderstatement and proof · cited by 6,410
Complexstatement and proof · cited by 5,565
StarRingstatement and proof · cited by 1,686
Inner.innerstatement · cited by 1,089
Normstatement and proof · cited by 512
NonUnitalSemiringstatement and proof · cited by 339
CStarModulestatement and proof · cited by 52

Cited by3

Results whose statement or proof uses this declaration.

WithCStarModule.norm_apply_le_normproof · cited by 2
WithCStarModule.max_le_prod_normproof · cited by 1
CStarModule.inner_mul_inner_swap_leproof · cited by 1