Documentation Verification Report

StarProjection

📁 Source: Mathlib/Algebra/Star/StarProjection.lean

Statistics

Metric	Count
Definitions `IsStarProjection`	1
Theorems `add`, `add_sub_mul_of_commute`, `isIdempotentElem`, `isSelfAdjoint`, `isStarNormal`, `mul`, `mul_one_sub_self`, `of_one_sub`, `one`, `one_sub`, `one_sub_mul_self`, `pow_eq`, `pow_succ_eq`, `sub_iff_mul_eq_left`, `sub_iff_mul_eq_right`, `sub_of_mul_eq_left`, `sub_of_mul_eq_right`, `zero`, `isStarProjection_iff`, `isStarProjection_iff'`, `isStarProjection_one_sub_iff`	21
Total	22

IsStarProjection

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add` 📖	mathematical	`IsStarProjection` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `StarRing.toStarAddMonoid` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	`Distrib.toAdd`	—	`IsIdempotentElem.add` `isIdempotentElem` `zero_add` `StarMul.star_mul` `IsSelfAdjoint.star_eq` `isSelfAdjoint` `star_zero` `IsSelfAdjoint.add`
`add_sub_mul_of_commute` 📖	mathematical	`Commute` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalRing.toNonUnitalNonAssocRing` `IsStarProjection` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `StarRing.toStarAddMonoid`	`SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `NonUnitalNonAssocRing.toAddCommGroup` `Distrib.toAdd`	—	`IsIdempotentElem.add_sub_mul_of_commute` `isIdempotentElem` `IsSelfAdjoint.sub` `IsSelfAdjoint.add` `isSelfAdjoint` `IsSelfAdjoint.commute_iff`
`isIdempotentElem` 📖	mathematical	`IsStarProjection`	`IsIdempotentElem`	—	—
`isSelfAdjoint` 📖	mathematical	`IsStarProjection`	`IsSelfAdjoint`	—	—
`isStarNormal` 📖	mathematical	`IsStarProjection`	`IsStarNormal`	—	`IsSelfAdjoint.isStarNormal` `isSelfAdjoint`
`mul` 📖	—	`IsStarProjection` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `StarRing.toStarAddMonoid` `Commute`	—	—	`IsIdempotentElem.mul_of_commute` `isIdempotentElem` `IsSelfAdjoint.commute_iff` `isSelfAdjoint`
`mul_one_sub_self` 📖	mathematical	`IsStarProjection` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing`	`SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `AddCommGroupWithOne.toAddGroupWithOne` `NonAssocRing.toAddCommGroupWithOne` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	—	`IsIdempotentElem.mul_one_sub_self` `isIdempotentElem`
`of_one_sub` 📖	—	`IsStarProjection` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `StarRing.toStarAddMonoid` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `AddCommGroupWithOne.toAddGroupWithOne` `NonAssocRing.toAddCommGroupWithOne` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne`	—	—	`isStarProjection_one_sub_iff`
`one` 📖	mathematical	—	`IsStarProjection` `MulOne.toMul` `MulOneClass.toMulOne` `InvolutiveStar.toStar` `StarMul.toInvolutiveStar` `MulOne.toOne`	—	`IsIdempotentElem.one` `IsSelfAdjoint.one`
`one_sub` 📖	mathematical	`IsStarProjection` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `StarRing.toStarAddMonoid`	`SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `AddCommGroupWithOne.toAddGroupWithOne` `NonAssocRing.toAddCommGroupWithOne` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne`	—	`IsIdempotentElem.one_sub` `isIdempotentElem` `IsSelfAdjoint.sub` `IsSelfAdjoint.one` `isSelfAdjoint`
`one_sub_mul_self` 📖	mathematical	`IsStarProjection` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing`	`SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `AddCommGroupWithOne.toAddGroupWithOne` `NonAssocRing.toAddCommGroupWithOne` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	—	`IsIdempotentElem.one_sub_mul_self` `isIdempotentElem`
`pow_eq` 📖	mathematical	`IsStarProjection` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass`	`Monoid.toNatPow`	—	`IsIdempotentElem.pow_eq` `isIdempotentElem`
`pow_succ_eq` 📖	mathematical	`IsStarProjection` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass`	`Monoid.toNatPow`	—	`IsIdempotentElem.pow_succ_eq` `isIdempotentElem`
`sub_iff_mul_eq_left` 📖	mathematical	`IsStarProjection` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalRing.toNonUnitalNonAssocRing` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `StarRing.toStarAddMonoid`	`SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `NonUnitalNonAssocRing.toAddCommGroup`	—	`isStarProjection_iff` `IsIdempotentElem.sub_iff` `isIdempotentElem` `IsSelfAdjoint.sub` `isSelfAdjoint` `StarMul.star_mul` `star_eq_iff_star_eq`
`sub_iff_mul_eq_right` 📖	mathematical	`IsStarProjection` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalRing.toNonUnitalNonAssocRing` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `StarRing.toStarAddMonoid`	`SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `NonUnitalNonAssocRing.toAddCommGroup`	—	`sub_iff_mul_eq_left` `StarMul.star_mul` `IsSelfAdjoint.star_eq` `isSelfAdjoint`
`sub_of_mul_eq_left` 📖	mathematical	`IsStarProjection` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `StarRing.toStarAddMonoid`	`SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `NonUnitalNonAssocRing.toAddCommGroup`	—	`IsIdempotentElem.sub` `isIdempotentElem` `StarMul.star_mul` `IsSelfAdjoint.star_eq` `isSelfAdjoint` `IsSelfAdjoint.sub`
`sub_of_mul_eq_right` 📖	mathematical	`IsStarProjection` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `StarRing.toStarAddMonoid`	`SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `NonUnitalNonAssocRing.toAddCommGroup`	—	`sub_of_mul_eq_left` `StarMul.star_mul` `IsSelfAdjoint.star_eq` `isSelfAdjoint`
`zero` 📖	mathematical	—	`IsStarProjection` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	—	`IsIdempotentElem.zero` `IsSelfAdjoint.zero`

(root)

Definitions

Name	Category	Theorems
`IsStarProjection` 📖	CompData	15 math math: `ContinuousLinearMap.isStarProjection_iff_isSymmetricProjection`, `IsStarProjection.one`, `isStarProjection_iff`, `isStarProjection_iff'`, `isStarProjection_one_sub_iff`, `InnerProductSpace.isStarProjection_rankOne_self`, `isStarProjection_starProjection`, `ContinuousLinearMap.isStarProjection_iff_isIdempotentElem_and_isStarNormal`, `LinearMap.isStarProjection_toContinuousLinearMap_iff`, `isStarProjection_iff_isIdempotentElem_and_isStarNormal`, `isStarProjection_iff_eq_starProjection_range`, `LinearMap.isStarProjection_iff_isSymmetricProjection`, `isStarProjection_iff_eq_starProjection`, `IsStarProjection.zero`, `ContinuousLinearMap.LinearMap.IsSymmetricProjection.isStarProjection`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isStarProjection_iff` 📖	mathematical	—	`IsStarProjection` `IsIdempotentElem` `IsSelfAdjoint`	—	—
`isStarProjection_iff'` 📖	mathematical	—	`IsStarProjection` `Star.star`	—	`isStarProjection_iff`
`isStarProjection_one_sub_iff` 📖	mathematical	—	`IsStarProjection` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `StarRing.toStarAddMonoid` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `AddCommGroupWithOne.toAddGroupWithOne` `NonAssocRing.toAddCommGroupWithOne` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne`	—	`IsStarProjection.one_sub` `sub_sub_cancel`

---

← Back to Index