feat(Analysis/CStarAlgebra): norms of sums of orthogonal selfadjoint elements

[j-loreaux]

---

• depends on: [Merged by Bors] - feat: norm of sums of continuous functions whose product is zero #36407
• depends on: feat: the Fuglede–Putnam–Rosenblum theorem for C⋆-algebras #37569

[github-actions]

PR summary d194281a48

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Algebra.Star.BigOperators	682	683	+1 (+0.15%)

Import changes for all files

Files

Import difference

803 files Mathlib.Algebra.AffineMonoid.Embedding Mathlib.Algebra.AffineMonoid.UniqueSums Mathlib.Algebra.Algebra.Subalgebra.IsSimpleOrder Mathlib.Algebra.BrauerGroup.Defs Mathlib.Algebra.Category.FGModuleCat.Abelian Mathlib.Algebra.Category.FGModuleCat.Basic Mathlib.Algebra.Category.FGModuleCat.Colimits Mathlib.Algebra.Category.FGModuleCat.EssentiallySmall Mathlib.Algebra.Category.FGModuleCat.Limits Mathlib.Algebra.Category.ModuleCat.Descent Mathlib.Algebra.Category.ModuleCat.ExteriorPower Mathlib.Algebra.Category.ModuleCat.Simple Mathlib.Algebra.Category.Ring.EqualizerPushout Mathlib.Algebra.Category.Ring.Under.Limits Mathlib.Algebra.DirectSum.LinearMap Mathlib.Algebra.GCDMonoid.IntegrallyClosed Mathlib.Algebra.Jordan.Basic Mathlib.Algebra.Lie.Abelian Mathlib.Algebra.Lie.AdjointAction.Basic Mathlib.Algebra.Lie.AdjointAction.Derivation Mathlib.Algebra.Lie.BaseChange Mathlib.Algebra.Lie.Basis Mathlib.Algebra.Lie.CartanExists Mathlib.Algebra.Lie.CartanSubalgebra Mathlib.Algebra.Lie.Character Mathlib.Algebra.Lie.Classical Mathlib.Algebra.Lie.Cochain Mathlib.Algebra.Lie.Derivation.BaseChange Mathlib.Algebra.Lie.Derivation.Basic Mathlib.Algebra.Lie.Derivation.Killing Mathlib.Algebra.Lie.DirectSum Mathlib.Algebra.Lie.EngelSubalgebra Mathlib.Algebra.Lie.Engel Mathlib.Algebra.Lie.Extension Mathlib.Algebra.Lie.Free Mathlib.Algebra.Lie.Graded Mathlib.Algebra.Lie.IdealOperations Mathlib.Algebra.Lie.Ideal Mathlib.Algebra.Lie.InvariantForm Mathlib.Algebra.Lie.Killing Mathlib.Algebra.Lie.LieTheorem Mathlib.Algebra.Lie.Loop Mathlib.Algebra.Lie.Matrix Mathlib.Algebra.Lie.Nilpotent Mathlib.Algebra.Lie.Normalizer Mathlib.Algebra.Lie.OfAssociative Mathlib.Algebra.Lie.Prod Mathlib.Algebra.Lie.Quotient Mathlib.Algebra.Lie.Rank Mathlib.Algebra.Lie.SemiDirect Mathlib.Algebra.Lie.Semisimple.Basic Mathlib.Algebra.Lie.Semisimple.Defs Mathlib.Algebra.Lie.Semisimple.Lemmas Mathlib.Algebra.Lie.SerreConstruction Mathlib.Algebra.Lie.SkewAdjoint Mathlib.Algebra.Lie.Sl2 Mathlib.Algebra.Lie.Solvable Mathlib.Algebra.Lie.Subalgebra Mathlib.Algebra.Lie.Submodule Mathlib.Algebra.Lie.TensorProduct Mathlib.Algebra.Lie.TraceForm Mathlib.Algebra.Lie.UniversalEnveloping Mathlib.Algebra.Lie.Weights.Basic Mathlib.Algebra.Lie.Weights.Cartan Mathlib.Algebra.Lie.Weights.Chain Mathlib.Algebra.Lie.Weights.IsSimple Mathlib.Algebra.Lie.Weights.Killing Mathlib.Algebra.Lie.Weights.Linear Mathlib.Algebra.Lie.Weights.RootSystem Mathlib.Algebra.LieRinehartAlgebra.Defs Mathlib.Algebra.Module.DedekindDomain Mathlib.Algebra.Module.Lattice Mathlib.Algebra.Module.LinearMap.Polynomial Mathlib.Algebra.Module.PID Mathlib.Algebra.Module.SpanRankOperations Mathlib.Algebra.Module.Submodule.Union Mathlib.Algebra.Module.Torsion.PrimaryComponent Mathlib.Algebra.MvPolynomial.Expand Mathlib.Algebra.MvPolynomial.Nilpotent Mathlib.Algebra.Order.Ring.StandardPart Mathlib.Algebra.Polynomial.Bivariate Mathlib.Algebra.Polynomial.Module.FiniteDimensional Mathlib.Algebra.Star.BigOperators Mathlib.Algebra.Star.LinearMap Mathlib.Algebra.Symmetrized Mathlib.AlgebraicGeometry.AffineScheme Mathlib.AlgebraicGeometry.AffineSpace Mathlib.AlgebraicGeometry.AffineTransitionLimit Mathlib.AlgebraicGeometry.AlgClosed.Basic Mathlib.AlgebraicGeometry.Artinian Mathlib.AlgebraicGeometry.ColimitsOver Mathlib.AlgebraicGeometry.Cover.Directed Mathlib.AlgebraicGeometry.Cover.MorphismProperty Mathlib.AlgebraicGeometry.Cover.Open Mathlib.AlgebraicGeometry.Cover.Over Mathlib.AlgebraicGeometry.Cover.QuasiCompact Mathlib.AlgebraicGeometry.Cover.Sigma Mathlib.AlgebraicGeometry.EffectiveEpi Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree Mathlib.AlgebraicGeometry.EllipticCurve.IsomOfJ Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point Mathlib.AlgebraicGeometry.EllipticCurve.Reduction Mathlib.AlgebraicGeometry.Fiber Mathlib.AlgebraicGeometry.FunctionField Mathlib.AlgebraicGeometry.GammaSpecAdjunction Mathlib.AlgebraicGeometry.Geometrically.Basic Mathlib.AlgebraicGeometry.Geometrically.Integral Mathlib.AlgebraicGeometry.Geometrically.Irreducible Mathlib.AlgebraicGeometry.Geometrically.Reduced Mathlib.AlgebraicGeometry.GluingOneHypercover Mathlib.AlgebraicGeometry.Gluing Mathlib.AlgebraicGeometry.Group.Abelian Mathlib.AlgebraicGeometry.Group.Smooth Mathlib.AlgebraicGeometry.IdealSheaf.Basic Mathlib.AlgebraicGeometry.IdealSheaf.Functorial Mathlib.AlgebraicGeometry.IdealSheaf.IrreducibleComponent Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme Mathlib.AlgebraicGeometry.LimitsOver Mathlib.AlgebraicGeometry.Limits Mathlib.AlgebraicGeometry.Modules.Presheaf Mathlib.AlgebraicGeometry.Modules.Sheaf Mathlib.AlgebraicGeometry.Modules.Tilde Mathlib.AlgebraicGeometry.Morphisms.AffineAnd Mathlib.AlgebraicGeometry.Morphisms.Affine Mathlib.AlgebraicGeometry.Morphisms.Basic Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion Mathlib.AlgebraicGeometry.Morphisms.Constructors Mathlib.AlgebraicGeometry.Morphisms.Descent Mathlib.AlgebraicGeometry.Morphisms.Etale Mathlib.AlgebraicGeometry.Morphisms.FinitePresentation Mathlib.AlgebraicGeometry.Morphisms.FiniteType Mathlib.AlgebraicGeometry.Morphisms.Finite Mathlib.AlgebraicGeometry.Morphisms.FlatDescent Mathlib.AlgebraicGeometry.Morphisms.FlatMono Mathlib.AlgebraicGeometry.Morphisms.Flat Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified Mathlib.AlgebraicGeometry.Morphisms.Immersion Mathlib.AlgebraicGeometry.Morphisms.Integral Mathlib.AlgebraicGeometry.Morphisms.IsIso Mathlib.AlgebraicGeometry.Morphisms.LocalClosure Mathlib.AlgebraicGeometry.Morphisms.LocalIso Mathlib.AlgebraicGeometry.Morphisms.OpenImmersion Mathlib.AlgebraicGeometry.Morphisms.Preimmersion Mathlib.AlgebraicGeometry.Morphisms.Proper Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties Mathlib.AlgebraicGeometry.Morphisms.SchemeTheoreticallyDominant Mathlib.AlgebraicGeometry.Morphisms.Separated Mathlib.AlgebraicGeometry.Morphisms.SmoothFiber Mathlib.AlgebraicGeometry.Morphisms.Smooth Mathlib.AlgebraicGeometry.Morphisms.SurjectiveOnStalks Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap Mathlib.AlgebraicGeometry.Morphisms.UniversallyClosed Mathlib.AlgebraicGeometry.Morphisms.UniversallyInjective Mathlib.AlgebraicGeometry.Morphisms.UniversallyOpen Mathlib.AlgebraicGeometry.Morphisms.WeaklyEtale Mathlib.AlgebraicGeometry.Noetherian Mathlib.AlgebraicGeometry.Normalization Mathlib.AlgebraicGeometry.OpenImmersion Mathlib.AlgebraicGeometry.Over Mathlib.AlgebraicGeometry.PointsPi Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Functor Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Proper Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme Mathlib.AlgebraicGeometry.Properties Mathlib.AlgebraicGeometry.PullbackCarrier Mathlib.AlgebraicGeometry.Pullbacks Mathlib.AlgebraicGeometry.QuasiAffine Mathlib.AlgebraicGeometry.RationalMap Mathlib.AlgebraicGeometry.RelativeGluing Mathlib.AlgebraicGeometry.ResidueField Mathlib.AlgebraicGeometry.Restrict Mathlib.AlgebraicGeometry.Scheme Mathlib.AlgebraicGeometry.Sites.BigZariski Mathlib.AlgebraicGeometry.Sites.ConstantSheaf Mathlib.AlgebraicGeometry.Sites.ElladicCohomology Mathlib.AlgebraicGeometry.Sites.Etale Mathlib.AlgebraicGeometry.Sites.Fpqc Mathlib.AlgebraicGeometry.Sites.MorphismProperty Mathlib.AlgebraicGeometry.Sites.Pretopology Mathlib.AlgebraicGeometry.Sites.Proetale Mathlib.AlgebraicGeometry.Sites.QuasiCompact Mathlib.AlgebraicGeometry.Sites.Representability Mathlib.AlgebraicGeometry.Sites.SheafQuasiCompact Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski Mathlib.AlgebraicGeometry.Sites.Small Mathlib.AlgebraicGeometry.Spec Mathlib.AlgebraicGeometry.SpreadingOut Mathlib.AlgebraicGeometry.Stalk Mathlib.AlgebraicGeometry.StructureSheaf Mathlib.AlgebraicGeometry.ValuativeCriterion Mathlib.AlgebraicGeometry.ZariskisMainTheorem Mathlib.Analysis.Analytic.Polynomial Mathlib.Analysis.Calculus.ImplicitFunction.ProdDomain Mathlib.Analysis.Calculus.Implicit Mathlib.Analysis.Calculus.LineDeriv.QuadraticMap Mathlib.Analysis.Convex.BetweenList Mathlib.Analysis.Convex.Between Mathlib.Analysis.Convex.Radon Mathlib.Analysis.Convex.Side Mathlib.Analysis.Convex.StrictConvexBetween Mathlib.Analysis.Convex.Visible Mathlib.Analysis.LocallyConvex.WeakDual Mathlib.Analysis.Normed.Field.WithAbs Mathlib.Analysis.Normed.Module.Bases Mathlib.Analysis.Normed.Module.Complemented Mathlib.Analysis.Normed.Module.ContinuousInverse Mathlib.Analysis.Real.Hyperreal Mathlib.CategoryTheory.Preadditive.HomOrthogonal Mathlib.CategoryTheory.Preadditive.Schur Mathlib.Combinatorics.Additive.ErdosGinzburgZiv Mathlib.Combinatorics.Optimization.ValuedCSP Mathlib.Combinatorics.SimpleGraph.AdjMatrix Mathlib.Combinatorics.SimpleGraph.StronglyRegular Mathlib.Data.Matrix.Block Mathlib.Data.Matrix.Cartan Mathlib.Data.Matrix.ColumnRowPartitioned Mathlib.Data.Matrix.Invertible Mathlib.Data.Matrix.Reflection Mathlib.Data.ZMod.QuotientRing Mathlib.Dynamics.Newton Mathlib.FieldTheory.AbelRuffini Mathlib.FieldTheory.AbsoluteGaloisGroup Mathlib.FieldTheory.AlgebraicClosure Mathlib.FieldTheory.AxGrothendieck Mathlib.FieldTheory.CardinalEmb Mathlib.FieldTheory.Cardinality Mathlib.FieldTheory.ChevalleyWarning Mathlib.FieldTheory.Differential.Basic Mathlib.FieldTheory.Differential.Liouville Mathlib.FieldTheory.Extension Mathlib.FieldTheory.Finite.Basic Mathlib.FieldTheory.Finite.Extension Mathlib.FieldTheory.Finite.GaloisField Mathlib.FieldTheory.Finite.Polynomial Mathlib.FieldTheory.Finite.Trace Mathlib.FieldTheory.Finite.Valuation Mathlib.FieldTheory.Fixed Mathlib.FieldTheory.Galois.Abelian Mathlib.FieldTheory.Galois.Basic Mathlib.FieldTheory.Galois.GaloisClosure Mathlib.FieldTheory.Galois.Infinite Mathlib.FieldTheory.Galois.IsGaloisGroup Mathlib.FieldTheory.Galois.NormalBasis Mathlib.FieldTheory.Galois.Profinite Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra Mathlib.FieldTheory.IntermediateField.Adjoin.Basic Mathlib.FieldTheory.IntermediateField.Algebraic Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure Mathlib.FieldTheory.IsAlgClosed.Basic Mathlib.FieldTheory.IsAlgClosed.Classification Mathlib.FieldTheory.IsAlgClosed.Spectrum Mathlib.FieldTheory.IsPerfectClosure Mathlib.FieldTheory.IsSepClosed Mathlib.FieldTheory.Isaacs Mathlib.FieldTheory.JacobsonNoether Mathlib.FieldTheory.KrullTopology Mathlib.FieldTheory.KummerExtension Mathlib.FieldTheory.KummerPolynomial Mathlib.FieldTheory.Laurent Mathlib.FieldTheory.LinearDisjoint Mathlib.FieldTheory.Minpoly.ConjRootClass Mathlib.FieldTheory.Minpoly.Field Mathlib.FieldTheory.Minpoly.IsConjRoot Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed Mathlib.FieldTheory.Minpoly.MinpolyDiv Mathlib.FieldTheory.Normal.Basic Mathlib.FieldTheory.Normal.Closure Mathlib.FieldTheory.Normal.Defs Mathlib.FieldTheory.NormalizedTrace Mathlib.FieldTheory.PerfectClosure Mathlib.FieldTheory.Perfect Mathlib.FieldTheory.PolynomialGaloisGroup Mathlib.FieldTheory.PrimitiveElement Mathlib.FieldTheory.PurelyInseparable.Basic Mathlib.FieldTheory.PurelyInseparable.Exponent Mathlib.FieldTheory.PurelyInseparable.PerfectClosure Mathlib.FieldTheory.PurelyInseparable.Tower Mathlib.FieldTheory.RatFunc.AsPolynomial Mathlib.FieldTheory.RatFunc.Basic Mathlib.FieldTheory.RatFunc.Degree Mathlib.FieldTheory.RatFunc.Luroth Mathlib.FieldTheory.Relrank Mathlib.FieldTheory.SeparableClosure Mathlib.FieldTheory.SeparableDegree Mathlib.FieldTheory.Separable Mathlib.FieldTheory.SeparablyGenerated Mathlib.FieldTheory.SplittingField.Construction Mathlib.FieldTheory.SplittingField.IsSplittingField Mathlib.Geometry.Convex.Cone.TensorProduct Mathlib.Geometry.Polygon.Basic Mathlib.GroupTheory.Coxeter.Basic Mathlib.GroupTheory.Coxeter.Inversion Mathlib.GroupTheory.Coxeter.Length Mathlib.GroupTheory.Coxeter.Matrix Mathlib.GroupTheory.FiniteAbelian.Basic Mathlib.GroupTheory.FiniteAbelian.Duality Mathlib.GroupTheory.SpecificGroups.ZGroup Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional Mathlib.LinearAlgebra.AffineSpace.Matrix Mathlib.LinearAlgebra.AnnihilatingPolynomial Mathlib.LinearAlgebra.BilinearForm.DualLattice Mathlib.LinearAlgebra.BilinearForm.Orthogonal Mathlib.LinearAlgebra.BilinearForm.Properties Mathlib.LinearAlgebra.BilinearForm.TensorProduct Mathlib.LinearAlgebra.Center Mathlib.LinearAlgebra.Charpoly.BaseChange Mathlib.LinearAlgebra.Charpoly.Basic Mathlib.LinearAlgebra.Charpoly.ToMatrix Mathlib.LinearAlgebra.CliffordAlgebra.BaseChange Mathlib.LinearAlgebra.CliffordAlgebra.Basic Mathlib.LinearAlgebra.CliffordAlgebra.CategoryTheory Mathlib.LinearAlgebra.CliffordAlgebra.Conjugation Mathlib.LinearAlgebra.CliffordAlgebra.Contraction Mathlib.LinearAlgebra.CliffordAlgebra.EvenEquiv Mathlib.LinearAlgebra.CliffordAlgebra.Even Mathlib.LinearAlgebra.CliffordAlgebra.Fold Mathlib.LinearAlgebra.CliffordAlgebra.Grading Mathlib.LinearAlgebra.CliffordAlgebra.Inversion Mathlib.LinearAlgebra.CliffordAlgebra.Prod Mathlib.LinearAlgebra.CliffordAlgebra.Star Mathlib.LinearAlgebra.Coevaluation Mathlib.LinearAlgebra.Contraction Mathlib.LinearAlgebra.CrossProduct Mathlib.LinearAlgebra.Determinant Mathlib.LinearAlgebra.Dual.BaseChange Mathlib.LinearAlgebra.Dual.Lemmas Mathlib.LinearAlgebra.Eigenspace.Basic Mathlib.LinearAlgebra.Eigenspace.Charpoly Mathlib.LinearAlgebra.Eigenspace.ContinuousLinearMap Mathlib.LinearAlgebra.Eigenspace.Matrix Mathlib.LinearAlgebra.Eigenspace.Minpoly Mathlib.LinearAlgebra.Eigenspace.Pi Mathlib.LinearAlgebra.Eigenspace.Semisimple Mathlib.LinearAlgebra.Eigenspace.Triangularizable Mathlib.LinearAlgebra.Eigenspace.Zero Mathlib.LinearAlgebra.ExteriorAlgebra.Basic Mathlib.LinearAlgebra.ExteriorAlgebra.Basis Mathlib.LinearAlgebra.ExteriorAlgebra.Grading Mathlib.LinearAlgebra.ExteriorAlgebra.OfAlternating Mathlib.LinearAlgebra.ExteriorPower.Basic Mathlib.LinearAlgebra.ExteriorPower.Basis Mathlib.LinearAlgebra.ExteriorPower.Pairing Mathlib.LinearAlgebra.FiniteDimensional.Basic Mathlib.LinearAlgebra.FiniteDimensional.Lemmas Mathlib.LinearAlgebra.FreeModule.Determinant Mathlib.LinearAlgebra.FreeModule.Finite.CardQuotient Mathlib.LinearAlgebra.FreeModule.Finite.Quotient Mathlib.LinearAlgebra.FreeModule.IdealQuotient Mathlib.LinearAlgebra.FreeModule.Int Mathlib.LinearAlgebra.FreeModule.Norm Mathlib.LinearAlgebra.FreeModule.PID Mathlib.LinearAlgebra.GeneralLinearGroup.AlgEquiv Mathlib.LinearAlgebra.JordanChevalley Mathlib.LinearAlgebra.Lagrange Mathlib.LinearAlgebra.Matrix.AbsoluteValue Mathlib.LinearAlgebra.Matrix.Adjugate Mathlib.LinearAlgebra.Matrix.BaseChange Mathlib.LinearAlgebra.Matrix.Basis Mathlib.LinearAlgebra.Matrix.BilinearForm Mathlib.LinearAlgebra.Matrix.Block Mathlib.LinearAlgebra.Matrix.Charpoly.Basic Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff Mathlib.LinearAlgebra.Matrix.Charpoly.Disc Mathlib.LinearAlgebra.Matrix.Charpoly.Eigs Mathlib.LinearAlgebra.Matrix.Charpoly.FiniteField Mathlib.LinearAlgebra.Matrix.Charpoly.LinearMap Mathlib.LinearAlgebra.Matrix.Charpoly.Minpoly Mathlib.LinearAlgebra.Matrix.Charpoly.Univ Mathlib.LinearAlgebra.Matrix.Circulant Mathlib.LinearAlgebra.Matrix.ConjTranspose Mathlib.LinearAlgebra.Matrix.Determinant.Basic Mathlib.LinearAlgebra.Matrix.Determinant.Misc Mathlib.LinearAlgebra.Matrix.Determinant.TotallyUnimodular Mathlib.LinearAlgebra.Matrix.Diagonal Mathlib.LinearAlgebra.Matrix.Dual Mathlib.LinearAlgebra.Matrix.FixedDetMatrices Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Basic Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Projective Mathlib.LinearAlgebra.Matrix.Gershgorin Mathlib.LinearAlgebra.Matrix.Hadamard Mathlib.LinearAlgebra.Matrix.Hermitian Mathlib.LinearAlgebra.Matrix.InvariantBasisNumber Mathlib.LinearAlgebra.Matrix.IsDiag Mathlib.LinearAlgebra.Matrix.Kronecker Mathlib.LinearAlgebra.Matrix.MvPolynomial Mathlib.LinearAlgebra.Matrix.Nondegenerate Mathlib.LinearAlgebra.Matrix.NonsingularInverse Mathlib.LinearAlgebra.Matrix.Notation Mathlib.LinearAlgebra.Matrix.Permanent Mathlib.LinearAlgebra.Matrix.Polynomial Mathlib.LinearAlgebra.Matrix.ProjectiveSpecialLinearGroup Mathlib.LinearAlgebra.Matrix.Reindex Mathlib.LinearAlgebra.Matrix.RowCol Mathlib.LinearAlgebra.Matrix.SchurComplement Mathlib.LinearAlgebra.Matrix.SesquilinearForm Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup Mathlib.LinearAlgebra.Matrix.Symmetric Mathlib.LinearAlgebra.Matrix.ToLin Mathlib.LinearAlgebra.Matrix.ToLinearEquiv Mathlib.LinearAlgebra.Matrix.Trace Mathlib.LinearAlgebra.Matrix.Transvection Mathlib.LinearAlgebra.Matrix.Vec Mathlib.LinearAlgebra.Matrix.WithConv Mathlib.LinearAlgebra.Matrix.ZPow Mathlib.LinearAlgebra.Orientation Mathlib.LinearAlgebra.PID Mathlib.LinearAlgebra.PerfectPairing.Basic Mathlib.LinearAlgebra.PerfectPairing.Restrict Mathlib.LinearAlgebra.Projectivization.Action Mathlib.LinearAlgebra.Projectivization.Basic Mathlib.LinearAlgebra.Projectivization.Cardinality Mathlib.LinearAlgebra.Projectivization.Independence Mathlib.LinearAlgebra.Projectivization.Subspace Mathlib.LinearAlgebra.QuadraticForm.AlgClosed Mathlib.LinearAlgebra.QuadraticForm.Basic Mathlib.LinearAlgebra.QuadraticForm.Basis Mathlib.LinearAlgebra.QuadraticForm.Dual Mathlib.LinearAlgebra.QuadraticForm.IsometryEquiv Mathlib.LinearAlgebra.QuadraticForm.Isometry Mathlib.LinearAlgebra.QuadraticForm.Prod Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat.Monoidal Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat.Symmetric Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat Mathlib.LinearAlgebra.QuadraticForm.Radical Mathlib.LinearAlgebra.QuadraticForm.Signature Mathlib.LinearAlgebra.QuadraticForm.TensorProduct.Isometries Mathlib.LinearAlgebra.QuadraticForm.TensorProduct Mathlib.LinearAlgebra.RootSystem.BaseChange Mathlib.LinearAlgebra.RootSystem.BaseExists Mathlib.LinearAlgebra.RootSystem.Base Mathlib.LinearAlgebra.RootSystem.Basic Mathlib.LinearAlgebra.RootSystem.CartanMatrix Mathlib.LinearAlgebra.RootSystem.Chain Mathlib.LinearAlgebra.RootSystem.Defs Mathlib.LinearAlgebra.RootSystem.Finite.CanonicalBilinear Mathlib.LinearAlgebra.RootSystem.Finite.G2 Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basic Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basis Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Lemmas Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Relations Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Semisimple Mathlib.LinearAlgebra.RootSystem.Hom Mathlib.LinearAlgebra.RootSystem.Irreducible Mathlib.LinearAlgebra.RootSystem.IsValuedIn Mathlib.LinearAlgebra.RootSystem.OfBilinear Mathlib.LinearAlgebra.RootSystem.Reduced Mathlib.LinearAlgebra.RootSystem.RootPairingCat Mathlib.LinearAlgebra.RootSystem.RootPositive Mathlib.LinearAlgebra.RootSystem.WeylGroup Mathlib.LinearAlgebra.Semisimple Mathlib.LinearAlgebra.Span.TensorProduct Mathlib.LinearAlgebra.SpecialLinearGroup Mathlib.LinearAlgebra.SymplecticGroup Mathlib.LinearAlgebra.TensorProduct.Matrix Mathlib.LinearAlgebra.Trace Mathlib.LinearAlgebra.Transvection.Basic Mathlib.LinearAlgebra.Transvection Mathlib.LinearAlgebra.Vandermonde Mathlib.MeasureTheory.Constructions.BorelSpace.ContinuousLinearMap Mathlib.MeasureTheory.Function.AEEqFun.DomAct Mathlib.MeasureTheory.Function.StronglyMeasurable.Lemmas Mathlib.ModelTheory.Algebra.Field.IsAlgClosed Mathlib.ModelTheory.Algebra.Ring.Definability Mathlib.ModelTheory.Arithmetic.Presburger.Definability Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter Mathlib.NumberTheory.DirichletCharacter.Bounds Mathlib.NumberTheory.FermatPsp Mathlib.NumberTheory.FrobeniusNumber Mathlib.NumberTheory.FunctionField Mathlib.NumberTheory.KummerDedekind Mathlib.NumberTheory.LegendreSymbol.Basic Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups Mathlib.NumberTheory.ModularForms.CongruenceSubgroups Mathlib.NumberTheory.NumberField.Basic Mathlib.NumberTheory.NumberField.Discriminant.Defs Mathlib.NumberTheory.NumberField.FractionalIdeal Mathlib.NumberTheory.NumberField.Ideal.KummerDedekind Mathlib.NumberTheory.NumberField.Norm Mathlib.NumberTheory.Padics.ProperSpace Mathlib.NumberTheory.Padics.RingHoms Mathlib.NumberTheory.PowModTotient Mathlib.NumberTheory.RamificationInertia.Basic Mathlib.NumberTheory.RamificationInertia.Galois Mathlib.NumberTheory.RamificationInertia.HilbertTheory Mathlib.NumberTheory.RamificationInertia.Inertia Mathlib.NumberTheory.RamificationInertia.Ramification Mathlib.NumberTheory.RamificationInertia.Unramified Mathlib.NumberTheory.RatFunc.Ostrowski Mathlib.NumberTheory.SumFourSquares Mathlib.NumberTheory.Wilson Mathlib.Probability.Independence.Process.HasIndepIncrements Mathlib.RepresentationTheory.Action Mathlib.RepresentationTheory.AlgebraRepresentation.Basic Mathlib.RepresentationTheory.Basic Mathlib.RepresentationTheory.Character Mathlib.RepresentationTheory.Coinduced Mathlib.RepresentationTheory.Coinvariants Mathlib.RepresentationTheory.Equiv Mathlib.RepresentationTheory.FDRep Mathlib.RepresentationTheory.FinGroupCharZero Mathlib.RepresentationTheory.FiniteIndex Mathlib.RepresentationTheory.Homological.FiniteCyclic Mathlib.RepresentationTheory.Homological.GroupCohomology.Basic Mathlib.RepresentationTheory.Homological.GroupCohomology.FiniteCyclic Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality Mathlib.RepresentationTheory.Homological.GroupCohomology.Hilbert90 Mathlib.RepresentationTheory.Homological.GroupCohomology.LongExactSequence Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree Mathlib.RepresentationTheory.Homological.GroupCohomology.Shapiro Mathlib.RepresentationTheory.Homological.GroupHomology.Basic Mathlib.RepresentationTheory.Homological.GroupHomology.FiniteCyclic Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality Mathlib.RepresentationTheory.Homological.GroupHomology.LongExactSequence Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree Mathlib.RepresentationTheory.Homological.GroupHomology.Shapiro Mathlib.RepresentationTheory.Homological.Resolution Mathlib.RepresentationTheory.Induced Mathlib.RepresentationTheory.Intertwining Mathlib.RepresentationTheory.Invariants Mathlib.RepresentationTheory.Irreducible Mathlib.RepresentationTheory.Maschke Mathlib.RepresentationTheory.Rep.Basic Mathlib.RepresentationTheory.Rep.Iso Mathlib.RepresentationTheory.Rep.Res Mathlib.RepresentationTheory.Semisimple Mathlib.RepresentationTheory.Submodule Mathlib.RepresentationTheory.Subrepresentation Mathlib.RepresentationTheory.Tannaka Mathlib.RingTheory.AdicCompletion.Completeness Mathlib.RingTheory.Adjoin.Field Mathlib.RingTheory.Adjoin.Polynomial.Bivariate Mathlib.RingTheory.Adjoin.PowerBasis Mathlib.RingTheory.AdjoinRoot Mathlib.RingTheory.Algebraic.Integral Mathlib.RingTheory.Algebraic.StronglyTranscendental Mathlib.RingTheory.AlgebraicIndependent.Adjoin Mathlib.RingTheory.AlgebraicIndependent.AlgebraicClosure Mathlib.RingTheory.AlgebraicIndependent.RankAndCardinality Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis Mathlib.RingTheory.Artinian.Algebra Mathlib.RingTheory.Artinian.Instances Mathlib.RingTheory.Artinian.Module Mathlib.RingTheory.Artinian.Ring Mathlib.RingTheory.ClassGroup Mathlib.RingTheory.Conductor Mathlib.RingTheory.DedekindDomain.AdicValuation Mathlib.RingTheory.DedekindDomain.Basic Mathlib.RingTheory.DedekindDomain.Different Mathlib.RingTheory.DedekindDomain.Dvr Mathlib.RingTheory.DedekindDomain.Factorization Mathlib.RingTheory.DedekindDomain.FiniteAdeleRing Mathlib.RingTheory.DedekindDomain.GaussLemma Mathlib.RingTheory.DedekindDomain.Ideal.Basic Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas Mathlib.RingTheory.DedekindDomain.Instances Mathlib.RingTheory.DedekindDomain.IntegralClosure Mathlib.RingTheory.DedekindDomain.LinearDisjoint Mathlib.RingTheory.DedekindDomain.PID Mathlib.RingTheory.DedekindDomain.SInteger Mathlib.RingTheory.DedekindDomain.SelmerGroup Mathlib.RingTheory.Derivation.Lie Mathlib.RingTheory.Derivation.MapCoeffs Mathlib.RingTheory.DiscreteValuationRing.TFAE Mathlib.RingTheory.Discriminant Mathlib.RingTheory.Etale.Basic Mathlib.RingTheory.Etale.Field Mathlib.RingTheory.Etale.Kaehler Mathlib.RingTheory.Etale.Locus Mathlib.RingTheory.Etale.Pi Mathlib.RingTheory.Etale.QuasiFinite Mathlib.RingTheory.Etale.StandardEtale Mathlib.RingTheory.Extension.Cotangent.Basis Mathlib.RingTheory.Extension.Cotangent.Free Mathlib.RingTheory.Extension.Cotangent.LocalizationAway Mathlib.RingTheory.Extension.Presentation.Core Mathlib.RingTheory.Extension.Presentation.Submersive Mathlib.RingTheory.FiniteLength Mathlib.RingTheory.Finiteness.Descent Mathlib.RingTheory.Finiteness.FinitePresentationLocal Mathlib.RingTheory.Finiteness.ModuleFinitePresentation Mathlib.RingTheory.Finiteness.NilpotentKer Mathlib.RingTheory.Finiteness.Nilpotent Mathlib.RingTheory.Flat.FaithfullyFlat.Algebra Mathlib.RingTheory.Flat.FaithfullyFlat.Descent Mathlib.RingTheory.Flat.TorsionFree Mathlib.RingTheory.FractionalIdeal.Extended Mathlib.RingTheory.FractionalIdeal.Norm Mathlib.RingTheory.Frobenius Mathlib.RingTheory.Grassmannian Mathlib.RingTheory.HopkinsLevitzki Mathlib.RingTheory.Ideal.AssociatedPrime.Localization Mathlib.RingTheory.Ideal.GoingDown Mathlib.RingTheory.Ideal.GoingUp Mathlib.RingTheory.Ideal.Height Mathlib.RingTheory.Ideal.Int Mathlib.RingTheory.Ideal.KrullsHeightTheorem Mathlib.RingTheory.Ideal.NatInt Mathlib.RingTheory.Ideal.Norm.AbsNorm Mathlib.RingTheory.Ideal.Norm.RelNorm Mathlib.RingTheory.Ideal.Pure Mathlib.RingTheory.Ideal.Quotient.HasFiniteQuotients Mathlib.RingTheory.Ideal.Quotient.Nilpotent Mathlib.RingTheory.IntegralClosure.Algebra.Basic Mathlib.RingTheory.IntegralClosure.Algebra.Ideal Mathlib.RingTheory.IntegralClosure.GoingDown Mathlib.RingTheory.IntegralClosure.IntegralRestrict Mathlib.RingTheory.IntegralClosure.IntegrallyClosed Mathlib.RingTheory.IntegralClosure.IsIntegral.AlmostIntegral Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic Mathlib.RingTheory.Invariant.Basic Mathlib.RingTheory.Invariant.Profinite Mathlib.RingTheory.IsAdjoinRoot Mathlib.RingTheory.Jacobson.Artinian Mathlib.RingTheory.Jacobson.Ring Mathlib.RingTheory.KrullDimension.Basic Mathlib.RingTheory.KrullDimension.Field Mathlib.RingTheory.KrullDimension.LocalRing Mathlib.RingTheory.KrullDimension.Module Mathlib.RingTheory.KrullDimension.NonZeroDivisors Mathlib.RingTheory.KrullDimension.PID Mathlib.RingTheory.KrullDimension.Polynomial Mathlib.RingTheory.KrullDimension.Regular Mathlib.RingTheory.KrullDimension.Zero Mathlib.RingTheory.LaurentSeries Mathlib.RingTheory.Length Mathlib.RingTheory.LinearDisjoint Mathlib.RingTheory.LocalProperties.IntegrallyClosed Mathlib.RingTheory.LocalProperties.Semilocal Mathlib.RingTheory.LocalRing.Module Mathlib.RingTheory.LocalRing.Quotient Mathlib.RingTheory.LocalRing.ResidueField.Fiber Mathlib.RingTheory.LocalRing.ResidueField.Instances Mathlib.RingTheory.LocalRing.ResidueField.Polynomial Mathlib.RingTheory.Localization.AtPrime.Extension Mathlib.RingTheory.Localization.Away.AdjoinRoot Mathlib.RingTheory.Localization.Integral Mathlib.RingTheory.Localization.NormTrace Mathlib.RingTheory.Localization.Pi Mathlib.RingTheory.MatrixAlgebra Mathlib.RingTheory.MatrixPolynomialAlgebra Mathlib.RingTheory.MvPolynomial.Expand Mathlib.RingTheory.MvPolynomial.IrreducibleQuadratic Mathlib.RingTheory.MvPowerSeries.Expand Mathlib.RingTheory.Nilpotent.GeometricallyReduced Mathlib.RingTheory.Nilpotent.Lemmas Mathlib.RingTheory.NoetherNormalization Mathlib.RingTheory.Noetherian.Nilpotent Mathlib.RingTheory.Norm.Basic Mathlib.RingTheory.Norm.Defs Mathlib.RingTheory.Norm.Transitivity Mathlib.RingTheory.NormTrace Mathlib.RingTheory.NormalClosure Mathlib.RingTheory.Nullstellensatz Mathlib.RingTheory.OrderOfVanishing Mathlib.RingTheory.PicardGroup Mathlib.RingTheory.Polynomial.DegreeLT Mathlib.RingTheory.Polynomial.GaussLemma Mathlib.RingTheory.Polynomial.IrreducibleRing Mathlib.RingTheory.Polynomial.IsIntegral Mathlib.RingTheory.Polynomial.Nilpotent Mathlib.RingTheory.Polynomial.RationalRoot Mathlib.RingTheory.Polynomial.Resultant.Basic Mathlib.RingTheory.Polynomial.SeparableDegree Mathlib.RingTheory.Polynomial.UniversalFactorizationRing Mathlib.RingTheory.PowerBasis Mathlib.RingTheory.PowerSeries.Expand Mathlib.RingTheory.QuasiFinite.Basic Mathlib.RingTheory.QuasiFinite.Polynomial Mathlib.RingTheory.QuasiFinite.Weakly Mathlib.RingTheory.Regular.Depth Mathlib.RingTheory.Regular.Flat Mathlib.RingTheory.Regular.RegularSequence Mathlib.RingTheory.RegularLocalRing.Defs Mathlib.RingTheory.RingHom.Etale Mathlib.RingTheory.RingHom.FaithfullyFlat Mathlib.RingTheory.RingHom.FinitePresentation Mathlib.RingTheory.RingHom.Flat Mathlib.RingTheory.RingHom.Integral Mathlib.RingTheory.RingHom.LocallyStandardSmooth Mathlib.RingTheory.RingHom.QuasiFinite Mathlib.RingTheory.RingHom.Smooth Mathlib.RingTheory.RingHom.StandardSmooth Mathlib.RingTheory.RingHom.Unramified Mathlib.RingTheory.RootsOfUnity.Lemmas Mathlib.RingTheory.RootsOfUnity.Minpoly Mathlib.RingTheory.SimpleModule.IsAlgClosed Mathlib.RingTheory.SimpleModule.Rank Mathlib.RingTheory.SimpleModule.WedderburnArtin Mathlib.RingTheory.Smooth.AdicCompletion Mathlib.RingTheory.Smooth.Basic Mathlib.RingTheory.Smooth.Fiber Mathlib.RingTheory.Smooth.Field Mathlib.RingTheory.Smooth.Flat Mathlib.RingTheory.Smooth.IntegralClosure Mathlib.RingTheory.Smooth.Local Mathlib.RingTheory.Smooth.Locus Mathlib.RingTheory.Smooth.NoetherianDescent Mathlib.RingTheory.Smooth.Pi Mathlib.RingTheory.Smooth.StandardSmoothCotangent Mathlib.RingTheory.Smooth.StandardSmoothOfFree Mathlib.RingTheory.Smooth.StandardSmooth Mathlib.RingTheory.Spectrum.Maximal.Localization Mathlib.RingTheory.Spectrum.Maximal.Topology Mathlib.RingTheory.Spectrum.Prime.Basic Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity Mathlib.RingTheory.Spectrum.Prime.Chevalley Mathlib.RingTheory.Spectrum.Prime.ConstructibleSet Mathlib.RingTheory.Spectrum.Prime.FreeLocus Mathlib.RingTheory.Spectrum.Prime.Homeomorph Mathlib.RingTheory.Spectrum.Prime.IsOpenComapC Mathlib.RingTheory.Spectrum.Prime.Jacobson Mathlib.RingTheory.Spectrum.Prime.LTSeries Mathlib.RingTheory.Spectrum.Prime.Module Mathlib.RingTheory.Spectrum.Prime.Noetherian Mathlib.RingTheory.Spectrum.Prime.Polynomial Mathlib.RingTheory.Spectrum.Prime.RingHom Mathlib.RingTheory.Spectrum.Prime.TensorProduct Mathlib.RingTheory.Spectrum.Prime.Topology Mathlib.RingTheory.Support Mathlib.RingTheory.TensorProduct.Free Mathlib.RingTheory.TensorProduct.IncludeLeftSubRight Mathlib.RingTheory.TensorProduct.IsBaseChangeHom Mathlib.RingTheory.TotallySplit Mathlib.RingTheory.Trace.Basic Mathlib.RingTheory.Trace.Defs Mathlib.RingTheory.Trace.Quotient Mathlib.RingTheory.UniqueFactorizationDomain.ClassGroup Mathlib.RingTheory.Unramified.Basic Mathlib.RingTheory.Unramified.Dedekind Mathlib.RingTheory.Unramified.Field Mathlib.RingTheory.Unramified.Finite Mathlib.RingTheory.Unramified.LocalRing Mathlib.RingTheory.Unramified.LocalStructure Mathlib.RingTheory.Unramified.Locus Mathlib.RingTheory.Unramified.Pi Mathlib.RingTheory.Valuation.AlgebraInstances Mathlib.RingTheory.Valuation.Discrete.Basic Mathlib.RingTheory.Valuation.Extension Mathlib.RingTheory.Valuation.FiniteField Mathlib.RingTheory.Valuation.Integral Mathlib.RingTheory.Valuation.LocalSubring Mathlib.RingTheory.Valuation.Minpoly Mathlib.RingTheory.Valuation.RamificationGroup Mathlib.RingTheory.Valuation.ValuationSubring Mathlib.RingTheory.WittVector.Basic Mathlib.RingTheory.WittVector.Compare Mathlib.RingTheory.WittVector.Complete Mathlib.RingTheory.WittVector.Defs Mathlib.RingTheory.WittVector.DiscreteValuationRing Mathlib.RingTheory.WittVector.Domain Mathlib.RingTheory.WittVector.FrobeniusFractionField Mathlib.RingTheory.WittVector.Frobenius Mathlib.RingTheory.WittVector.Identities Mathlib.RingTheory.WittVector.InitTail Mathlib.RingTheory.WittVector.IsPoly Mathlib.RingTheory.WittVector.Isocrystal Mathlib.RingTheory.WittVector.MulCoeff Mathlib.RingTheory.WittVector.MulP Mathlib.RingTheory.WittVector.StructurePolynomial Mathlib.RingTheory.WittVector.TeichmullerSeries Mathlib.RingTheory.WittVector.Teichmuller Mathlib.RingTheory.WittVector.Truncated Mathlib.RingTheory.WittVector.Verschiebung Mathlib.RingTheory.WittVector.WittPolynomial Mathlib.RingTheory.ZMod.Torsion Mathlib.RingTheory.ZMod Mathlib.RingTheory.ZariskisMainTheorem Mathlib.Topology.Algebra.AsymptoticCone Mathlib.Topology.Algebra.Group.Matrix Mathlib.Topology.Algebra.Module.Determinant Mathlib.Topology.Algebra.Module.FiniteDimensionBilinear Mathlib.Topology.Algebra.Module.FiniteDimension Mathlib.Topology.Algebra.Module.TopDualPairing Mathlib.Topology.Algebra.Ring.Compact Mathlib.Topology.Algebra.Star.LinearMap Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology Mathlib.Topology.Algebra.Valued.ValuationTopology Mathlib.Topology.Algebra.Valued.ValuativeRel Mathlib.Topology.Algebra.Valued.ValuedField Mathlib.Topology.Algebra.Valued.WithVal Mathlib.Topology.Algebra.Valued.WithZeroMulInt Mathlib.Topology.Compactification.OnePoint.ProjectiveLine Mathlib.Topology.Instances.Matrix

1

---

Declarations diff

+ IsSelfAdjoint.commute_of_mul_eq_zero
++ nnnorm_sum_eq_sup
+++ nnnorm_add_eq_max
+++ nnnorm_sub_eq_max
+++ norm_add_eq_max
+++ norm_sub_eq_max

You can run this locally as follows

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

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

The doc-module for scripts/pr_summary/declarations_diff.sh contains some details about this script.

---

No changes to technical debt.

You can run this locally as

./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).

[github-actions]

✅ PR Title Formatted Correctly

The title of this PR has been updated to match our commit style conventions.
Thank you!

[mathlib-dependent-issues]

This PR/issue depends on:

• [Merged by Bors] - feat: norm of sums of continuous functions whose product is zero #36407
• feat: the Fuglede–Putnam–Rosenblum theorem for C⋆-algebras #37569
  By Dependent Issues (🤖). Happy coding!

[mathlib-merge-conflicts]

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

[grunweg]

Hello from PR triage --- this PR does not have an area label. Can you add one, please? (I'm not sure which one is best here, t-analysis?)

[loefflerd]

Maybe a comment in the proof to explain the strategy might be helpful, "we show that the closed subalgebra generated by a and b is commutative and apply CommCStarAlgebra.norm_add_eq_max to this subalgebra" or something.

(By the way: I was slightly puzzled that this statement does not actually imply the commutative version, because you have IsSelfAdjoint. Perhaps one could split up the argument here into two lemmas, one assuming instead that a, b are normal and a * b = b * a = 0 – which would then imply the commutative lemma – and then showing separately that if a, b are selfadjoint then it suffices to assume just a * b = 0. Just a suggestion, I'm no expert in this theory so I can't really judge whether this additional generality is useful.)

[j-loreaux]

@loefflerd thanks for the review! I have added a brief explanation.

Indeed, this does not imply the commutative version. The reason I didn't originally state it for IsStarNormal is that you need two commuting hypotheses (Commute a b and Commute a (star b)), and moreover, the IsSelfAdjoint version is the one that almost always appears in practice.

That being said, it's not unreasonable to have the IsStarNormal variants, so I have added them (except the Finset.sum version; at that point, I claim the user should just move to the commutative C⋆-subalgebra and work there, because the hypotheses get rather unwieldy). I have also added the lemma that selfadjoint elements whose product is zero commute, and then use it to prove the selfadjoint versions from the normal versions. This could of course generalize a bit further (e.g., selfadjoint elements whose product is selfadjoint and lies in the center of the algebra commute, but that's a rather uncommon scenario), but we opt not to add that since it isn't as useful.

[loefflerd]

The reason I didn't originally state it for IsStarNormal is that you need two commuting hypotheses (Commute a b and Commute a (star b)),

Doesn't the second Commute hypothesis follow from first by the Fuglede-Putnam theorem? (Maybe mathlib doesn't have this yet though.)

[j-loreaux]

Right, we don't have it. I think we may have all the tools necessary though. I'll look into it.

[j-loreaux]

Indeed, I have a proof of Fuglede–Putnam–Rosenblum now. I'll create a PR for that first.

[loefflerd]

Great! The statement of Fuglede–Putnam is pretty much the sole thing I remember from the Banach Algebras course I took decades ago as a masters student, so it's nice to see it make its way into mathlib :-)

[j-loreaux]

#37569