feat(Analysis/CStarAlgebra/Extreme): a C⋆-algebra is unital iff there exists an extreme point in the closed unit ball

[themathqueen]

Co-authored-by: Jon Bannon 59937998+JonBannon@users.noreply.github.com
Co-authored-by: Jireh Loreaux loreaujy@gmail.com

---

• depends on: [Merged by Bors] - feat(Analysis/CStarAlgebra/CFC/Order): conjugating with a star projection in a C*-algebra #35997
• depends on: [Merged by Bors] - feat(Analysis/CStarAlgebra): set of star projections equals the extreme points of the nonnegative closed unit ball #36201
• depends on: [Merged by Bors] - feat: norm of sums of continuous functions whose product is zero #36407
• depends on: [Merged by Bors] - feat: properties of the real and imaginary parts in a complex star module #36408
• depends on: [Merged by Bors] - feat(Analysis/CStarAlgebra): norms of sums of orthogonal selfadjoint elements #36416
• depends on: [Merged by Bors] - feat(Analysis/Convex/Strict/Extreme): extremePoints ℝ (Icc a b) = {a, b} #36603
• depends on: feat(Algebra): IsUnital and IsNotUnital classes #41923

[github-actions]

PR summary 5569c7c2b1

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Analysis.CStarAlgebra.Extreme	2787	2797	+10 (+0.36%)

Import changes for all files

Files	Import difference
Mathlib.Analysis.CStarAlgebra.Extreme	10

---

Declarations diff (regex)

+ CStarAlgebra.isNotUnital_iff
+ CStarAlgebra.isUnital_iff
+ CStarAlgebra.mul_ofExtremePtOne
+ CStarAlgebra.ofExtremePtOne_mul
+ CStarAlgebra.one_mem_extremePoints_unitClosedBall
+ IsNotUnital
+ IsUnital
+ IsUnital.toAlgebra
+ IsUnital.toCStarAlgebra
+ IsUnital.toCommCStarAlgebra
+ IsUnital.toMonoid
+ IsUnital.toMulOneClass
+ MulOneClass.isUnital
+ Unitary.coe_mem_extremePoints_unitClosedBall
+ eq_zero_of_eq_sub_of_mem_closedBall_of_mem_extremePoints_closedUnitBall
+ isStarProjection_self_mul_star_of_mem_extremePoints_closedUnitBall
+ isStarProjection_star_mul_self_of_mem_extremePoints_closedUnitBall
+ not_isNotUnital_iff_isUnital
+ not_isUnital_iff_isNotUnital
+ star_mem_extremePoints_closedBall_zero_iff
+ star_self_conjugate_eq_self_of_mem_extremePoints_closedUnitBall
+ toCommRing
+ toCommSemiring
+ toNonAssocCommRing
+ toNonAssocCommSemiring
+ toNonAssocRing
+ toNonAssocSemiring
+ toRing
+ toSemiring

You can run this locally as follows

## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

## summary with just the declaration names:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

Declarations diff (Lean)

✅ Lean-aware diff — post-build, computed from the Lean environment (commit 5569c7c).

• +41 new declarations
• −0 removed declarations

+CStarAlgebra.isNotUnital_iff
+CStarAlgebra.isUnital_iff
+CStarAlgebra.mul_ofExtremePtOne
+CStarAlgebra.ofExtremePtOne_mul
+CStarAlgebra.one_mem_extremePoints_unitClosedBall
+IsNotUnital
+IsNotUnital.casesOn
+IsNotUnital.isNotUnital
+IsNotUnital.mk
+IsNotUnital.rec
+IsNotUnital.recOn
+IsUnital
+IsUnital.casesOn
+IsUnital.isUnital
+IsUnital.mk
+IsUnital.rec
+IsUnital.recOn
+IsUnital.toAlgebra
+IsUnital.toCStarAlgebra
+IsUnital.toCommCStarAlgebra
+IsUnital.toCommRing
+IsUnital.toCommSemiring
+IsUnital.toMonoid
+IsUnital.toMulOneClass
+IsUnital.toNonAssocCommRing
+IsUnital.toNonAssocCommSemiring
+IsUnital.toNonAssocRing
+IsUnital.toNonAssocSemiring
+IsUnital.toRing
+IsUnital.toSemiring
+MulOneClass.isUnital
+Unitary.coe_mem_extremePoints_unitClosedBall
+isNotUnital_iff
+isStarProjection_self_mul_star_of_mem_extremePoints_closedUnitBall
+isStarProjection_star_mul_self_of_mem_extremePoints_closedUnitBall
+isUnital_iff
+not_isNotUnital_iff_isUnital
+not_isUnital_iff_isNotUnital
+quasispectrum.norm_le_norm_of_mem
+star_mem_extremePoints_closedBall_zero_iff
+star_self_conjugate_eq_self_of_mem_extremePoints_closedUnitBall

---

No changes to strong technical debt.

Increase in weak tech debt: (relative, absolute) = (1.00, 0.20)

Current number	Change	Type (weak)
5	1	large files

Current commit 5569c7c2b1
Reference commit 8c79cb4f54

This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:

git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/scripts/reporting/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[mathlib-merge-conflicts]

This pull request has conflicts, please merge master and resolve them.

[mathlib-merge-conflicts]

This pull request has conflicts, please merge master and resolve them.

[mathlib-dependent-issues]

This PR/issue depends on:

• [Merged by Bors] - feat(Analysis/CStarAlgebra/CFC/Order): conjugating with a star projection in a C*-algebra #35997
• [Merged by Bors] - feat(Analysis/CStarAlgebra): set of star projections equals the extreme points of the nonnegative closed unit ball #36201
• [Merged by Bors] - feat: norm of sums of continuous functions whose product is zero #36407
• [Merged by Bors] - feat: properties of the real and imaginary parts in a complex star module #36408
• [Merged by Bors] - feat(Analysis/CStarAlgebra): norms of sums of orthogonal selfadjoint elements #36416
• [Merged by Bors] - feat(Analysis/Convex/Strict/Extreme): extremePoints ℝ (Icc a b) = {a, b} #36603
• feat(Algebra): IsUnital and IsNotUnital classes #41923
  By Dependent Issues (🤖). Happy coding!

[mathlib-merge-conflicts]

This pull request has conflicts, please merge master and resolve them.