Theorems · Definition · functional analysis
IsStrictlyPositive
{A : Type u_1} → [LE A] → [Monoid A] → [Zero A] → A → PropAn element of an ordered algebra is strictly positive if it is nonnegative and invertible. NOTE: This definition will be generalized to the non-unital case in the future; do not unfold the definition and use the API provided instead to avoid breakage when the refactor happens.
- Defined in
- Mathlib.Algebra.Algebra.StrictPositivity
- Cited by
- 75 results in Mathlib
- Foundations
- Depth 4 from the axioms · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites2
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
Cited by75
Results whose statement or proof uses this declaration.
- IsStrictlyPositive.nonnegstatement and proof · cited by 18
- IsStrictlyPositive.isUnitstatement and proof · cited by 12
- CStarAlgebra.isStrictlyPositive_TFAEstatement and proof · cited by 7
- IsStrictlyPositive.iff_of_unitalstatement · cited by 7
- CFC.rpow_rpowstatement and proof · cited by 6
- IsUnit.isStrictlyPositivestatement · cited by 5
- CFC.inverse_eq_rpow_neg_onestatement and proof · cited by 4
- IsStrictlyPositive.of_lestatement and proof · cited by 4
- IsStrictlyPositive.spectrum_posstatement and proof · cited by 4
- CStarAlgebra.isUnit_of_lestatement and proof · cited by 3
- Units.isStrictlyPositive_iffstatement and proof · cited by 3
- CFC.monotoneOn_one_sub_one_add_invproof · cited by 2