Mathlib Map

Theorems · Theorem · functional analysis

star_nonneg_iff

∀ {R : Type u_1} [inst : NonUnitalSemiring R] [inst_1 : PartialOrder R] [inst_2 : StarRing R] [StarOrderedRing R]
  {x : R}, 0 ≤ star x ↔ 0 ≤ x
Defined in
Mathlib.Algebra.Order.Star.Basic
Cited by
1 results in Mathlib
Foundations
Depth 66 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes
NonUnitalSemiringPartialOrderStarRingStarOrderedRing
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

RCLike.wInner_nonneg · cited by 0RCLike.wInner_nonnegPartialOrder · cited by 6410PartialOrderStarRing · cited by 1686StarRingStar.star · cited by 1082Star.starStarOrderedRing · cited by 587StarOrderedRingNonUnitalSemiring · cited by 339NonUnitalSemiringstar_zero · cited by 58star_zerostar_le_star_iff · cited by 6star_le_star_iffstar_nonneg_iffCITED BYCITES

Cites7

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

Cited by1

Results whose statement or proof uses this declaration.