Theorems · Theorem · functional analysis
StarOrderedRing.le_iff
∀ {R : Type u_3} {inst : NonUnitalSemiring R} {inst_1 : PartialOrder R} {inst_2 : StarRing R} [self : StarOrderedRing R]
(x y : R), x ≤ y ↔ ∃ p ∈ AddSubmonoid.closure (Set.range fun s => star s * s), y = x + pcharacterization of the order in terms of the StarRing structure.
- Defined in
- Mathlib.Algebra.Order.Star.Basic
- Cited by
- 5 results in Mathlib
- Foundations
- Depth 16 from the axioms · uses propext, Quot.sound
- Assumes
- StarOrderedRing
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites8
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- PartialOrderstatement and proof · cited by 6,410
- Set.rangestatement · cited by 4,705
- StarRingstatement and proof · cited by 1,686
- AddSubmonoidstatement · cited by 1,178
- Star.starstatement · cited by 1,082
- StarOrderedRingstatement and proof · cited by 587
- NonUnitalSemiringstatement and proof · cited by 339
- AddSubmonoid.closurestatement · cited by 224
Cited by5
Results whose statement or proof uses this declaration.
- star_le_star_iffproof · cited by 6
- star_left_conjugate_le_conjugateproof · cited by 6
- IsSelfAdjoint.of_geproof · cited by 2
- NonUnitalStarRingHom.map_le_map_of_map_starproof · cited by 0
- StarOrderedRing.lt_iffproof · cited by 0