Basic

📁 Source: Mathlib/Algebra/Order/Star/Basic.lean

Statistics

Metric	Count
Definitions `StarOrderedRing`	1
Theorems `conjugate_le_conjugate`, `conjugate_nonneg`, `mono`, `mul_self_nonneg`, `of_nonneg`, `sq_nonneg`, `le_of_mul_eq_left`, `le_of_mul_eq_right`, `le_one`, `mem_Icc`, `nonneg`, `one_sub_nonneg`, `star_left_conjugate_nonneg_iff`, `star_right_conjugate_nonneg_iff`, `isSelfAdjoint`, `star_eq`, `instStarOrderedRing`, `instStarOrderedRing`, `map_le_map_of_map_star`, `le_iff`, `lt_iff`, `nonneg_iff`, `of_le_iff`, `of_nonneg_iff`, `of_nonneg_iff'`, `pos_iff`, `toExistsAddOfLE`, `toIsOrderedAddMonoid`, `instOrderIsoClass`, `instOrderHomClass`, `conjugate_le_conjugate`, `conjugate_le_conjugate'`, `conjugate_le_conjugate_of_nonneg`, `conjugate_lt_conjugate`, `conjugate_lt_conjugate'`, `conjugate_nonneg`, `conjugate_nonneg'`, `conjugate_nonneg_of_nonneg`, `conjugate_pos`, `conjugate_pos'`, `instIsOrderedModule`, `instIsStrictOrderedModuleOfIsCancelAdd`, `instPosSMulStrictMono`, `instZeroLEOneClass`, `mul_star_self_nonneg`, `mul_star_self_pos`, `one_le_star_iff`, `one_lt_star_iff`, `smul_mem_closure_star_mul`, `star_le_iff`, `star_le_one_iff`, `star_le_star_iff`, `star_left_conjugate_le_conjugate`, `star_left_conjugate_lt_conjugate`, `star_left_conjugate_nonneg`, `star_left_conjugate_pos`, `star_lt_iff`, `star_lt_one_iff`, `star_lt_star_iff`, `star_mul_self_nonneg`, `star_mul_self_pos`, `star_neg_iff`, `star_nonneg_iff`, `star_nonpos_iff`, `star_pos_iff`, `star_right_conjugate_le_conjugate`, `star_right_conjugate_lt_conjugate`, `star_right_conjugate_nonneg`, `star_right_conjugate_pos`	69
Total	70

IsSelfAdjoint

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`conjugate_le_conjugate` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `IsSelfAdjoint` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `StarRing.toStarAddMonoid`	`Preorder.toLE` `PartialOrder.toPreorder` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalSemiring.toNonUnitalNonAssocSemiring`	—	`star_eq` `star_left_conjugate_le_conjugate`
`conjugate_nonneg` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `IsSelfAdjoint` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `StarRing.toStarAddMonoid`	`Preorder.toLE` `PartialOrder.toPreorder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	—	`star_right_conjugate_nonneg`
`mono` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `IsSelfAdjoint` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `StarRing.toStarAddMonoid`	`IsSelfAdjoint` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `StarRing.toStarAddMonoid`	—	`StarOrderedRing.le_iff` `eq_1` `StarAddMonoid.star_add` `star_eq` `AddMonoidHom.eqOn_closureM` `AddEquivClass.instAddMonoidHomClass` `AddEquiv.instAddEquivClass` `StarMul.star_mul` `star_star`
`mul_self_nonneg` 📖	mathematical	`IsSelfAdjoint` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `StarRing.toStarAddMonoid`	`Preorder.toLE` `PartialOrder.toPreorder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	—	`star_eq` `star_mul_self_nonneg`
`of_nonneg` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalSemiring.toNonUnitalNonAssocSemiring`	`IsSelfAdjoint` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `StarRing.toStarAddMonoid`	—	`mono` `zero`
`sq_nonneg` 📖	mathematical	`IsSelfAdjoint` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `StarRing.toStarAddMonoid`	`Preorder.toLE` `PartialOrder.toPreorder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Monoid.toPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero`	—	`sq` `mul_self_nonneg`

IsStarProjection

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`le_of_mul_eq_left` 📖	mathematical	`IsStarProjection` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalRing.toNonUnitalNonAssocRing` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `StarRing.toStarAddMonoid`	`Preorder.toLE` `PartialOrder.toPreorder`	—	`sub_nonneg` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedCancelAddMonoid.toIsOrderedAddMonoid` `IsOrderedAddMonoid.toIsOrderedCancelAddMonoid` `StarOrderedRing.toIsOrderedAddMonoid` `nonneg` `sub_of_mul_eq_left`
`le_of_mul_eq_right` 📖	mathematical	`IsStarProjection` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalRing.toNonUnitalNonAssocRing` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `StarRing.toStarAddMonoid`	`Preorder.toLE` `PartialOrder.toPreorder`	—	`sub_nonneg` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedCancelAddMonoid.toIsOrderedAddMonoid` `IsOrderedAddMonoid.toIsOrderedCancelAddMonoid` `StarOrderedRing.toIsOrderedAddMonoid` `nonneg` `sub_of_mul_eq_right`
`le_one` 📖	mathematical	`IsStarProjection` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `StarRing.toStarAddMonoid`	`Preorder.toLE` `PartialOrder.toPreorder` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne`	—	`sub_nonneg` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedCancelAddMonoid.toIsOrderedAddMonoid` `IsOrderedAddMonoid.toIsOrderedCancelAddMonoid` `StarOrderedRing.toIsOrderedAddMonoid` `one_sub_nonneg`
`mem_Icc` 📖	mathematical	`IsStarProjection` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `StarRing.toStarAddMonoid`	`Set` `Set.instMembership` `Set.Icc` `PartialOrder.toPreorder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne`	—	`nonneg` `le_one`
`nonneg` 📖	mathematical	`IsStarProjection` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `StarRing.toStarAddMonoid`	`Preorder.toLE` `PartialOrder.toPreorder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalSemiring.toNonUnitalNonAssocSemiring`	—	`IsSelfAdjoint.mul_self_nonneg` `isSelfAdjoint` `isIdempotentElem`
`one_sub_nonneg` 📖	mathematical	`IsStarProjection` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `StarRing.toStarAddMonoid`	`Preorder.toLE` `PartialOrder.toPreorder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne`	—	`nonneg` `one_sub`

IsUnit

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`star_left_conjugate_nonneg_iff` 📖	mathematical	`IsUnit` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero`	`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` `star_right_conjugate_nonneg_iff` `star`
`star_right_conjugate_nonneg_iff` 📖	mathematical	`IsUnit` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero`	`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`	—	`exists_left_inv` `star_right_conjugate_nonneg` `mul_one` `star_one` `StarMul.star_mul` `mul_assoc` `one_mul`

LE.le

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isSelfAdjoint` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalSemiring.toNonUnitalNonAssocSemiring`	`IsSelfAdjoint` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `StarRing.toStarAddMonoid`	—	`IsSelfAdjoint.of_nonneg`
`star_eq` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalSemiring.toNonUnitalNonAssocSemiring`	`Star.star` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `StarRing.toStarAddMonoid`	—	`IsSelfAdjoint.star_eq` `isSelfAdjoint`

MulOpposite

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instStarOrderedRing` 📖	mathematical	—	`StarOrderedRing` `MulOpposite` `instNonUnitalSemiring` `instPartialOrder` `instStarRing`	—	`unop_le_unop` `StarOrderedRing.le_iff` `Function.Surjective.exists` `op_surjective` `AddEquivClass.instAddMonoidHomClass` `AddEquiv.instAddEquivClass` `AddSubmonoid.comap_map_eq_of_injective` `AddEquiv.injective` `AddSubmonoid.comap.congr_simp` `AddMonoidHom.map_mclosure` `Set.image_congr` `Function.Surjective.range_comp` `Function.Involutive.surjective` `InvolutiveStar.star_involutive` `star_star`

Nat

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instStarOrderedRing` 📖	mathematical	—	`StarOrderedRing` `instNonUnitalSemiring` `instPartialOrder` `instStarRing`	—	`eq_top_mono` `AddSubmonoid.closure_mono` `Set.singleton_subset_iff` `Set.mem_range` `one_mul` `addSubmonoidClosure_one` `instCanonicallyOrderedAdd` `TrivialStar.star_trivial` `instTrivialStar`

NonUnitalStarRingHom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`map_le_map_of_map_star` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder`	`Preorder.toLE` `PartialOrder.toPreorder` `DFunLike.coe` `NonUnitalStarRingHom` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `StarRing.toStarAddMonoid` `instFunLike`	—	`StarOrderedRing.le_iff` `StarHomClass.map_star` `NonUnitalStarRingHomClass.toStarHomClass` `instNonUnitalRingHomClass` `instNonUnitalStarRingHomClass` `AddSubmonoid.closure_induction` `map_mul` `NonUnitalRingHomClass.toMulHomClass` `AddSubmonoid.mem_closure_of_mem` `map_zero` `AddMonoidHomClass.toZeroHomClass` `NonUnitalRingHomClass.toAddMonoidHomClass` `AddSubmonoidClass.toZeroMemClass` `AddSubmonoid.instAddSubmonoidClass` `map_add` `AddMonoidHomClass.toAddHomClass` `AddMemClass.add_mem` `AddSubmonoidClass.toAddMemClass`

StarOrderedRing

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`le_iff` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder` `AddSubmonoid` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `SetLike.instMembership` `AddSubmonoid.instSetLike` `AddSubmonoid.closure` `Set.range` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `Star.star` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `StarRing.toStarAddMonoid` `Distrib.toAdd`	—	—
`lt_iff` 📖	mathematical	—	`Preorder.toLT` `PartialOrder.toPreorder` `AddSubmonoid` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `SetLike.instMembership` `AddSubmonoid.instSetLike` `AddSubmonoid.closure` `Set.range` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `Star.star` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `StarRing.toStarAddMonoid` `Distrib.toAdd`	—	`lt_iff_le_and_ne` `le_iff` `IsCancelAdd.toIsLeftCancelAdd`
`nonneg_iff` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `AddSubmonoid` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `SetLike.instMembership` `AddSubmonoid.instSetLike` `AddSubmonoid.closure` `Set.range` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `Star.star` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `StarRing.toStarAddMonoid`	—	`zero_add`
`of_le_iff` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Distrib.toMul` `Star.star` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `StarRing.toStarAddMonoid`	`StarOrderedRing`	—	`AddSubmonoid.subset_closure` `AddSubmonoid.closure_induction` `Eq.ge` `add_zero` `add_assoc` `LE.le.trans`
`of_nonneg_iff` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalRing.toNonUnitalNonAssocRing` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `AddSubmonoid` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `NonUnitalNonAssocRing.toAddCommGroup` `SetLike.instMembership` `AddSubmonoid.instSetLike` `AddSubmonoid.closure` `Set.range` `Distrib.toMul` `Star.star` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `StarRing.toStarAddMonoid`	`StarOrderedRing` `NonUnitalRing.toNonUnitalSemiring`	—	`covariant_swap_add_of_covariant_add`
`of_nonneg_iff'` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalRing.toNonUnitalNonAssocRing` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `Distrib.toMul` `Star.star` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `StarRing.toStarAddMonoid`	`StarOrderedRing` `NonUnitalRing.toNonUnitalSemiring`	—	`of_le_iff` `covariant_swap_add_of_covariant_add`
`pos_iff` 📖	mathematical	—	`Preorder.toLT` `PartialOrder.toPreorder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `AddSubmonoid` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `SetLike.instMembership` `AddSubmonoid.instSetLike` `AddSubmonoid.closure` `Set.range` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `Star.star` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `StarRing.toStarAddMonoid`	—	`zero_add`
`toExistsAddOfLE` 📖	mathematical	—	`ExistsAddOfLE` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Preorder.toLE` `PartialOrder.toPreorder`	—	`le_iff`
`toIsOrderedAddMonoid` 📖	mathematical	—	`IsOrderedAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `PartialOrder.toPreorder`	—	`le_iff` `add_right_comm`

StarRingEquivClass

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instOrderIsoClass` 📖	mathematical	—	`OrderIsoClass` `Preorder.toLE` `PartialOrder.toPreorder`	—	`RingEquivClass.toNonUnitalRingHomClass` `StarRingEquiv.instRingEquivClass` `instNonUnitalStarRingHomClass` `StarRingEquiv.instStarRingEquivClass` `toRingEquivClass` `EquivLike.inv_apply_apply` `NonUnitalStarRingHom.map_le_map_of_map_star` `RelHomClass.map_rel` `StarRingHomClass.instOrderHomClass`

StarRingHomClass

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instOrderHomClass` 📖	mathematical	—	`OrderHomClass` `Preorder.toLE` `PartialOrder.toPreorder`	—	`NonUnitalStarRingHom.map_le_map_of_map_star`

(root)

Definitions

Name	Category	Theorems
`StarOrderedRing` 📖	CompData	21 math math: `Prod.instStarOrderedRing`, `Real.instStarOrderedRing`, `StarOrderedRing.of_nonneg_iff'`, `RCLike.toStarOrderedRing`, `NNRat.instStarOrderedRing`, `MulOpposite.instStarOrderedRing`, `CStarMatrix.instStarOrderedRing`, `Unitization.instStarOrderedRing`, `ContinuousLinearMap.instStarOrderedRing`, `ContinuousMapZero.instStarOrderedRing`, `ContinuousMap.instStarOrderedRingOfContinuousSqrt`, `NNReal.instStarOrderedRing`, `Nat.instStarOrderedRing`, `Int.instStarOrderedRing`, `StarOrderedRing.of_nonneg_iff`, `StarOrderedRing.of_le_iff`, `CStarAlgebra.spectralOrderedRing`, `Rat.instStarOrderedRing`, `Matrix.instStarOrderedRing`, `ContinuousLinearMap.instStarOrderedRingRCLike`, `Pi.instStarOrderedRing`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`conjugate_le_conjugate` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder`	`Preorder.toLE` `PartialOrder.toPreorder` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Star.star` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `StarRing.toStarAddMonoid`	—	`star_left_conjugate_le_conjugate`
`conjugate_le_conjugate'` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder`	`Preorder.toLE` `PartialOrder.toPreorder` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Star.star` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `StarRing.toStarAddMonoid`	—	`star_right_conjugate_le_conjugate`
`conjugate_le_conjugate_of_nonneg` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalSemiring.toNonUnitalNonAssocSemiring`	`Preorder.toLE` `PartialOrder.toPreorder` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalSemiring.toNonUnitalNonAssocSemiring`	—	`IsSelfAdjoint.conjugate_le_conjugate` `IsSelfAdjoint.of_nonneg`
`conjugate_lt_conjugate` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `IsRegular` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalSemiring.toNonUnitalNonAssocSemiring`	`Preorder.toLT` `PartialOrder.toPreorder` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Star.star` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `StarRing.toStarAddMonoid`	—	`star_left_conjugate_lt_conjugate`
`conjugate_lt_conjugate'` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `IsRegular` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalSemiring.toNonUnitalNonAssocSemiring`	`Preorder.toLT` `PartialOrder.toPreorder` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Star.star` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `StarRing.toStarAddMonoid`	—	`star_right_conjugate_lt_conjugate`
`conjugate_nonneg` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalSemiring.toNonUnitalNonAssocSemiring`	`Preorder.toLE` `PartialOrder.toPreorder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `Star.star` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `StarRing.toStarAddMonoid`	—	`star_left_conjugate_nonneg`
`conjugate_nonneg'` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalSemiring.toNonUnitalNonAssocSemiring`	`Preorder.toLE` `PartialOrder.toPreorder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `Star.star` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `StarRing.toStarAddMonoid`	—	`star_right_conjugate_nonneg`
`conjugate_nonneg_of_nonneg` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalSemiring.toNonUnitalNonAssocSemiring`	`Preorder.toLE` `PartialOrder.toPreorder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	—	`IsSelfAdjoint.conjugate_nonneg` `IsSelfAdjoint.of_nonneg`
`conjugate_pos` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `IsRegular` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	`Preorder.toLT` `PartialOrder.toPreorder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `Star.star` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `StarRing.toStarAddMonoid`	—	`star_left_conjugate_pos`
`conjugate_pos'` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `IsRegular` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	`Preorder.toLT` `PartialOrder.toPreorder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `Star.star` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `StarRing.toStarAddMonoid`	—	`star_right_conjugate_pos`
`instIsOrderedModule` 📖	mathematical	—	`IsOrderedModule` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `PartialOrder.toPreorder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	—	`StarOrderedRing.le_iff` `smul_mem_closure_star_mul` `StarOrderedRing.nonneg_iff` `smul_add` `add_smul`
`instIsStrictOrderedModuleOfIsCancelAdd` 📖	mathematical	—	`IsStrictOrderedModule` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `PartialOrder.toPreorder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	—	`instPosSMulStrictMono` `StarOrderedRing.lt_iff` `StarOrderedRing.pos_iff` `smul_ne_zero` `IsDomain.toIsCancelMulZero` `smul_mem_closure_star_mul` `add_smul`
`instPosSMulStrictMono` 📖	mathematical	—	`PosSMulStrictMono` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `PartialOrder.toPreorder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	—	`StarOrderedRing.lt_iff` `StarOrderedRing.pos_iff` `smul_ne_zero` `IsDomain.toIsCancelMulZero` `smul_mem_closure_star_mul` `smul_add`
`instZeroLEOneClass` 📖	mathematical	—	`ZeroLEOneClass` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Preorder.toLE` `PartialOrder.toPreorder`	—	`star_one` `mul_one` `star_mul_self_nonneg`
`mul_star_self_nonneg` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `Star.star` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `StarRing.toStarAddMonoid`	—	`star_star` `star_mul_self_nonneg`
`mul_star_self_pos` 📖	mathematical	`IsRegular` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalSemiring.toNonUnitalNonAssocSemiring`	`Preorder.toLT` `PartialOrder.toPreorder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `Star.star` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `StarRing.toStarAddMonoid`	—	`star_star` `star_mul_self_pos` `IsRegular.star`
`one_le_star_iff` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `Star.star` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `StarRing.toStarAddMonoid`	—	`star_one` `star_le_star_iff`
`one_lt_star_iff` 📖	mathematical	—	`Preorder.toLT` `PartialOrder.toPreorder` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `Star.star` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `StarRing.toStarAddMonoid`	—	`star_one` `star_lt_star_iff`
`smul_mem_closure_star_mul` 📖	mathematical	`AddSubmonoid` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `SetLike.instMembership` `AddSubmonoid.instSetLike` `AddSubmonoid.closure` `Set.range` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Star.star` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `StarRing.toStarAddMonoid` `NonUnitalSemiring.toNonUnitalNonAssocSemiring`	`AddSubmonoid` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `SetLike.instMembership` `AddSubmonoid.instSetLike` `AddSubmonoid.closure` `Set.range` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `Star.star` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `StarRing.toStarAddMonoid` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction`	—	`AddSubmonoid.closure_induction` `AddSubmonoid.subset_closure` `StarModule.star_smul` `smul_mul_smul_comm` `IsScalarTower.left` `smul_zero` `AddSubmonoidClass.toZeroMemClass` `AddSubmonoid.instAddSubmonoidClass` `smul_add` `AddMemClass.add_mem` `AddSubmonoidClass.toAddMemClass` `zero_smul` `add_smul`
`star_le_iff` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder` `Star.star` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `StarRing.toStarAddMonoid`	—	`star_le_star_iff` `star_star`
`star_le_one_iff` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder` `Star.star` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `StarRing.toStarAddMonoid` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	—	`star_one` `star_le_star_iff`
`star_le_star_iff` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder` `Star.star` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `StarRing.toStarAddMonoid`	—	`StarOrderedRing.le_iff` `AddMonoidHom.mclosure_preimage_le` `AddEquivClass.instAddMonoidHomClass` `AddEquiv.instAddEquivClass` `AddSubmonoid.closure_mono` `StarMul.star_mul` `star_star` `StarAddMonoid.star_add`
`star_left_conjugate_le_conjugate` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder`	`Preorder.toLE` `PartialOrder.toPreorder` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Star.star` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `StarRing.toStarAddMonoid`	—	`StarOrderedRing.le_iff` `star_left_conjugate_nonneg` `mul_add` `Distrib.leftDistribClass` `add_mul` `Distrib.rightDistribClass`
`star_left_conjugate_lt_conjugate` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `IsRegular` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalSemiring.toNonUnitalNonAssocSemiring`	`Preorder.toLT` `PartialOrder.toPreorder` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Star.star` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `StarRing.toStarAddMonoid`	—	`LE.le.lt_iff_ne` `star_left_conjugate_le_conjugate` `LT.lt.le` `IsRegular.right` `IsRegular.left` `IsRegular.star` `LT.lt.ne`
`star_left_conjugate_nonneg` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalSemiring.toNonUnitalNonAssocSemiring`	`Preorder.toLE` `PartialOrder.toPreorder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `Star.star` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `StarRing.toStarAddMonoid`	—	`AddSubmonoid.closure_induction` `StarMul.star_mul` `mul_assoc` `star_mul_self_nonneg` `MulZeroClass.mul_zero` `MulZeroClass.zero_mul` `le_refl` `add_zero` `add_le_add_right` `IsOrderedAddMonoid.toAddLeftMono` `StarOrderedRing.toIsOrderedAddMonoid` `mul_add` `Distrib.leftDistribClass` `add_mul` `Distrib.rightDistribClass` `StarOrderedRing.nonneg_iff`
`star_left_conjugate_pos` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `IsRegular` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	`Preorder.toLT` `PartialOrder.toPreorder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `Star.star` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `StarRing.toStarAddMonoid`	—	`MulZeroClass.mul_zero` `MulZeroClass.zero_mul` `star_left_conjugate_lt_conjugate`
`star_lt_iff` 📖	mathematical	—	`Preorder.toLT` `PartialOrder.toPreorder` `Star.star` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `StarRing.toStarAddMonoid`	—	`star_lt_star_iff` `star_star`
`star_lt_one_iff` 📖	mathematical	—	`Preorder.toLT` `PartialOrder.toPreorder` `Star.star` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `StarRing.toStarAddMonoid` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	—	`star_one` `star_lt_star_iff`
`star_lt_star_iff` 📖	mathematical	—	`Preorder.toLT` `PartialOrder.toPreorder` `Star.star` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `StarRing.toStarAddMonoid`	—	`star_le_star_iff`
`star_mul_self_nonneg` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `Star.star` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `StarRing.toStarAddMonoid`	—	`StarOrderedRing.nonneg_iff` `AddSubmonoid.subset_closure`
`star_mul_self_pos` 📖	mathematical	`IsRegular` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalSemiring.toNonUnitalNonAssocSemiring`	`Preorder.toLT` `PartialOrder.toPreorder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `Star.star` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `StarRing.toStarAddMonoid`	—	`LE.le.lt_iff_ne` `star_mul_self_nonneg` `MulZeroClass.mul_zero` `IsRegular.left` `IsRegular.star` `IsRegular.ne_zero`
`star_neg_iff` 📖	mathematical	—	`Preorder.toLT` `PartialOrder.toPreorder` `Star.star` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `StarRing.toStarAddMonoid` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	—	`star_zero` `star_lt_star_iff`
`star_nonneg_iff` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Star.star` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `StarRing.toStarAddMonoid`	—	`star_zero` `star_le_star_iff`
`star_nonpos_iff` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder` `Star.star` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `StarRing.toStarAddMonoid` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	—	`star_zero` `star_le_star_iff`
`star_pos_iff` 📖	mathematical	—	`Preorder.toLT` `PartialOrder.toPreorder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Star.star` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `StarRing.toStarAddMonoid`	—	`star_zero` `star_lt_star_iff`
`star_right_conjugate_le_conjugate` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder`	`Preorder.toLE` `PartialOrder.toPreorder` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Star.star` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `StarRing.toStarAddMonoid`	—	`star_star` `star_left_conjugate_le_conjugate`
`star_right_conjugate_lt_conjugate` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `IsRegular` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalSemiring.toNonUnitalNonAssocSemiring`	`Preorder.toLT` `PartialOrder.toPreorder` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Star.star` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `StarRing.toStarAddMonoid`	—	`star_star` `star_left_conjugate_lt_conjugate` `IsRegular.star`
`star_right_conjugate_nonneg` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalSemiring.toNonUnitalNonAssocSemiring`	`Preorder.toLE` `PartialOrder.toPreorder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `Star.star` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `StarRing.toStarAddMonoid`	—	`star_star` `star_left_conjugate_nonneg`
`star_right_conjugate_pos` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `IsRegular` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	`Preorder.toLT` `PartialOrder.toPreorder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `Star.star` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `StarRing.toStarAddMonoid`	—	`star_star` `star_left_conjugate_pos` `IsRegular.star`

---

← Back to Index