Documentation Verification Report

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_algebraMap`, `isStrictlyPositive_one`	11
Total	12

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` `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`	`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` `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` `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` `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`

(root)

Definitions

Name	Category	Theorems
`IsStrictlyPositive` 📖	MathDef	21 math math: `IsUnit.isStrictlyPositive_star_right_conjugate_iff`, `isStrictlyPositive_one`, `CStarAlgebra.isStrictlyPositive_iff_exists_isUnit_and_isSelfAdjoint_and_eq_mul_self`, `isStrictlyPositive_algebraMap`, `CStarAlgebra.isStrictlyPositive_iff_isStrictlyPositive_sqrt_and_eq_sqrt_mul_sqrt`, `CStarAlgebra.isStrictlyPositive_iff_eq_mul_star_self`, `IsUnit.isStrictlyPositive_star_left_conjugate_iff`, `CStarAlgebra.isStrictlyPositive_iff_exists_isStrictlyPositive_and_eq_mul_self`, `Matrix.isStrictlyPositive_iff_posDef`, `CFC.log_monotoneOn`, `IsStrictlyPositive.iff_of_unital`, `Matrix.PosDef.isStrictlyPositive`, `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`, `cfc_isStrictlyPositive_iff`, `StarOrderedRing.isStrictlyPositive_iff_spectrum_pos`, `CFC.continuousOn_rpow`

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` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `DFunLike.coe` `RingHom` `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