StrictPositivity

📁 Source: Mathlib/Algebra/Algebra/StrictPositivity.lean

Statistics

Metric	Count
Definitions IsStrictlyPositive	1
Theorems iff_of_unital, isSelfAdjoint, isUnit, nonneg, smul, spectrum_pos, isStrictlyPositive, isStrictlyPositive_star_left_conjugate_iff, isStrictlyPositive_star_right_conjugate_iff, isStrictlyPositive_iff, isStrictlyPositive_of_le, isStrictlyPositive_algebraMap, isStrictlyPositive_one	13
Total	14

IsStrictlyPositive

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
iff_of_unital 📖	mathematical	—	IsStrictlyPositive IsUnit	—	—
isSelfAdjoint 📖	mathematical	IsStrictlyPositive Preorder.toLE PartialOrder.toPreorder MonoidWithZero.toMonoid Semiring.toMonoidWithZero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	IsSelfAdjoint InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring StarRing.toStarAddMonoid	—	LE.le.isSelfAdjoint nonneg
isUnit 📖	mathematical	IsStrictlyPositive	IsUnit	—	—
nonneg 📖	—	IsStrictlyPositive	—	—	—
smul 📖	mathematical	Preorder.toLT PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring IsStrictlyPositive Preorder.toLE MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing	IsStrictlyPositive Preorder.toLE PartialOrder.toPreorder MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Algebra.toSMul Semifield.toCommSemiring	—	isUnit_iff_exists isUnit Algebra.mul_smul_comm Algebra.smul_mul_assoc IsUnit.mul_val_inv inv_smul_smul₀ ne_of_lt IsUnit.val_inv_mul smul_inv_smul₀ IsUnit.isStrictlyPositive smul_nonneg LT.lt.le nonneg
spectrum_pos 📖	mathematical	IsStrictlyPositive Preorder.toLE PartialOrder.toPreorder MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Set Set.instMembership spectrum	Preorder.toLT PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring	—	lt_of_le_of_ne

IsUnit

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isStrictlyPositive 📖	mathematical	IsUnit	IsStrictlyPositive	—	IsStrictlyPositive.iff_of_unital
isStrictlyPositive_star_left_conjugate_iff 📖	mathematical	IsUnit MonoidWithZero.toMonoid Semiring.toMonoidWithZero	IsStrictlyPositive Preorder.toLE PartialOrder.toPreorder MonoidWithZero.toMonoid Semiring.toMonoidWithZero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Distrib.toMul NonUnitalNonAssocSemiring.toDistrib Star.star InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid StarRing.toStarAddMonoid	—	star_star isStrictlyPositive_star_right_conjugate_iff star
isStrictlyPositive_star_right_conjugate_iff 📖	mathematical	IsUnit MonoidWithZero.toMonoid Semiring.toMonoidWithZero	IsStrictlyPositive Preorder.toLE PartialOrder.toPreorder MonoidWithZero.toMonoid Semiring.toMonoidWithZero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Distrib.toMul NonUnitalNonAssocSemiring.toDistrib Star.star InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid StarRing.toStarAddMonoid	—	star_right_conjugate_nonneg_iff CanLift.prf instCanLiftUnitsValIsUnit Units.coe_star Units.isUnit_mul_units Units.isUnit_units_mul

Units

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isStrictlyPositive_iff 📖	mathematical	—	IsStrictlyPositive val	—	IsStrictlyPositive.nonneg IsStrictlyPositive.iff_of_unital isUnit
isStrictlyPositive_of_le 📖	mathematical	val	IsStrictlyPositive val	—	isStrictlyPositive_iff

(root)

Definitions

Name	Category	Theorems
IsStrictlyPositive 📖	MathDef	32 math math: IsUnit.isStrictlyPositive_star_right_conjugate_iff, isStrictlyPositive_one, isStrictlyPositive_add, CStarAlgebra.isStrictlyPositive_iff_exists_isUnit_and_isSelfAdjoint_and_eq_mul_self, isStrictlyPositive_algebraMap, CStarAlgebra.isStrictlyPositive_iff_isStrictlyPositive_sqrt_and_eq_sqrt_mul_sqrt, IsStrictlyPositive.rpow, CStarAlgebra.isStrictlyPositive_iff_eq_mul_star_self, IsUnit.isStrictlyPositive_star_left_conjugate_iff, IsStrictlyPositive.smul, CStarAlgebra.isStrictlyPositive_iff_exists_isStrictlyPositive_and_eq_mul_self, Matrix.isStrictlyPositive_iff_posDef, CFC.log_monotoneOn, IsStrictlyPositive.nnrpow, IsStrictlyPositive.sqrt, IsStrictlyPositive.iff_of_unital, Matrix.PosDef.isStrictlyPositive, IsStrictlyPositive.commute_iff, IsUnit.isStrictlyPositive, CStarAlgebra.isStrictlyPositive_iff_isUnit_sqrt_and_eq_sqrt_mul_sqrt, cfcHom_isStrictlyPositive_iff, CStarAlgebra.isStrictlyPositive_iff_eq_star_mul_self, CStarAlgebra.isStrictlyPositive_TFAE, CStarAlgebra.isStrictlyPositive_iff_isSelfAdjoint_and_spectrum_pos, Units.isStrictlyPositive_iff, cfc_isStrictlyPositive_iff, Units.isStrictlyPositive_of_le, StarOrderedRing.isStrictlyPositive_iff_spectrum_pos, IsStrictlyPositive.add_nonneg, IsStrictlyPositive.of_le, CFC.continuousOn_rpow, IsStrictlyPositive.nonneg_add

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isStrictlyPositive_algebraMap 📖	mathematical	Preorder.toLT PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring	IsStrictlyPositive Preorder.toLE PartialOrder.toPreorder MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring Semifield.toCommSemiring RingHom.instFunLike algebraMap	—	Algebra.algebraMap_eq_smul_one IsStrictlyPositive.smul isStrictlyPositive_one
isStrictlyPositive_one 📖	mathematical	—	IsStrictlyPositive MulOne.toOne MulOneClass.toMulOne Monoid.toMulOneClass	—	IsStrictlyPositive.iff_of_unital zero_le_one isUnit_one

---

← Back to Index