Theorems · Theorem · functional analysis
LE.le.isSelfAdjoint
∀ {R : Type u_1} [inst : NonUnitalSemiring R] [inst_1 : PartialOrder R] [inst_2 : StarRing R] [StarOrderedRing R]
{x : R}, 0 ≤ x → IsSelfAdjoint xAn alias of IsSelfAdjoint.of_nonneg for use with dot notation.
- Defined in
- Mathlib.Algebra.Order.Star.Basic
- Cited by
- 20 results in Mathlib
- Foundations
- Depth 67 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites6
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- PartialOrderstatement · cited by 6,410
- StarRingstatement · cited by 1,686
- StarOrderedRingstatement · cited by 587
- IsSelfAdjointstatement · cited by 545
- NonUnitalSemiringstatement · cited by 339
- IsSelfAdjoint.of_nonnegproof · cited by 43
Cited by20
Results whose statement or proof uses this declaration.
- LE.le.star_eqproof · cited by 8
- CStarAlgebra.nonneg_TFAEproof · cited by 6
- nonneg_iff_realPart_imaginaryPartproof · cited by 3
- Commute.mul_nonnegproof · cited by 3
- ProbabilityTheory.covarianceBilin_multivariateGaussianproof · cited by 3
- IsStrictlyPositive.isSelfAdjointproof · cited by 2
- IsSelfAdjoint.iff_of_leproof · cited by 1
- commute_iff_mul_nonnegproof · cited by 1
- range_cfc_nnreal_subsetproof · cited by 1
- CFC.negPart_eq_of_eq_PosPart_subproof · cited by 1
- selfAdjoint.star_coe_unitarySelfAddISMulproof · cited by 0