feat(Analysis/Normed/Module/Complemented): The idempotent associated with a complemented subspace

[mans0954]

Given a complemented subspace p of a Banach space E, with complement q, there exists an idempotent P in the ring E →L[𝕜] E such that P has range p and kernel q. Similarly 1-P has range q and kernel p.

See Rudin, Functional Analysis, Theorem 5.16.

---

This PR continues the work from #20330.

Original PR: #20330

[mans0954]

Comments from Original PR #20330

This section contains 4 comment(s) from the original PR, excluding bot comments.

---

@github-actions (2024-12-29 18:35 UTC):

PR summary 8b2141b23d

Import changes exceeding 2%

%	File
+22.16%	Mathlib.Algebra.Module.End
+10.41%	Mathlib.Algebra.Module.Hom

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Algebra.Module.End	388	474	+86 (+22.16%)
Mathlib.Algebra.Module.Hom	442	488	+46 (+10.41%)
Mathlib.Algebra.Module.LinearMap.End	452	453	+1 (+0.22%)

Import changes for all files

Files	Import difference
11 files Mathlib.Algebra.Category.Grp.Kernels Mathlib.Algebra.ModEq Mathlib.Algebra.Module.LinearMap.End Mathlib.Algebra.Module.Submodule.EqLocus Mathlib.Algebra.Module.Submodule.Equiv Mathlib.Algebra.Module.Submodule.IterateMapComap Mathlib.Algebra.Module.Submodule.Ker Mathlib.Algebra.Module.Submodule.LinearMap Mathlib.Algebra.Module.Submodule.Map Mathlib.Algebra.Module.Submodule.Range Mathlib.GroupTheory.ClassEquation	1
Mathlib.Algebra.Module.Submodule.Invariant	2
Mathlib.LinearAlgebra.Matrix.SemiringInverse Mathlib.RingTheory.Localization.Integer	3
21 files Mathlib.Algebra.Order.Antidiag.Nat Mathlib.Algebra.Polynomial.Basic Mathlib.Algebra.Polynomial.Cardinal Mathlib.Algebra.Polynomial.Eval.Algebra Mathlib.Algebra.Polynomial.Eval.Defs Mathlib.Algebra.Polynomial.Monomial Mathlib.Algebra.Ring.CentroidHom Mathlib.Algebra.Squarefree.Basic Mathlib.Algebra.Star.CentroidHom Mathlib.Computability.TMComputable Mathlib.Data.Nat.Squarefree Mathlib.NumberTheory.ArithmeticFunction Mathlib.NumberTheory.MaricaSchoenheim Mathlib.NumberTheory.SmoothNumbers Mathlib.RingTheory.Localization.Defs Mathlib.RingTheory.OreLocalization.Cardinality Mathlib.RingTheory.Radical Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet Mathlib.RingTheory.UniqueFactorizationDomain.Finsupp Mathlib.RingTheory.UniqueFactorizationDomain.GCDMonoid Mathlib.SetTheory.Surreal.Dyadic	4
18 files Mathlib.Algebra.DirectSum.Basic Mathlib.Algebra.DirectSum.Ring Mathlib.Algebra.MonoidAlgebra.Defs Mathlib.Algebra.MonoidAlgebra.Division Mathlib.Algebra.MonoidAlgebra.MapDomain Mathlib.Algebra.MonoidAlgebra.NoZeroDivisors Mathlib.Algebra.SkewMonoidAlgebra.Basic Mathlib.Analysis.Normed.Group.Submodule Mathlib.Data.DFinsupp.Submonoid Mathlib.Dynamics.Flow Mathlib.Dynamics.OmegaLimit Mathlib.LinearAlgebra.Finsupp.LSum Mathlib.RingTheory.Nilpotent.Basic Mathlib.RingTheory.OreLocalization.Ring Mathlib.Topology.Algebra.GroupWithZero Mathlib.Topology.Algebra.Monoid Mathlib.Topology.Algebra.WithZeroTopology Mathlib.Topology.ApproximateUnit	5
19 files Mathlib.Combinatorics.Enumerative.Bell Mathlib.Data.DFinsupp.Interval Mathlib.Data.Finsupp.Antidiagonal Mathlib.Data.Finsupp.Interval Mathlib.Data.Finsupp.MonomialOrder Mathlib.Data.Finsupp.Multiset Mathlib.Data.Finsupp.WellFounded Mathlib.Data.Multiset.Interval Mathlib.Data.Nat.Choose.Factorization Mathlib.Data.Nat.Choose.Multinomial Mathlib.Data.Nat.Factorization.Basic Mathlib.Data.Nat.Factorization.Defs Mathlib.Data.Nat.Factorization.Induction Mathlib.Data.Nat.Factorization.PrimePow Mathlib.Data.Nat.Factorization.Root Mathlib.Logic.Hydra Mathlib.SetTheory.Cardinal.Finsupp Mathlib.SetTheory.Surreal.Multiplication Mathlib.Topology.Algebra.Algebra.Rat	7
7 files Mathlib.Algebra.Order.Floor.Div Mathlib.Analysis.Normed.Group.Subgroup Mathlib.Data.DFinsupp.BigOperators Mathlib.Data.DFinsupp.Multiset Mathlib.Data.Finsupp.Lex Mathlib.Data.Finsupp.Order Mathlib.Data.Finsupp.PWO	8
Mathlib.Analysis.NormedSpace.MStructure	10
70 files Mathlib.Algebra.BigOperators.Balance Mathlib.Algebra.BigOperators.Expect Mathlib.Algebra.Order.BigOperators.Expect Mathlib.AlgebraicTopology.MooreComplex Mathlib.Analysis.BoxIntegral.Box.Basic Mathlib.Analysis.BoxIntegral.Partition.Basic Mathlib.Analysis.BoxIntegral.Partition.Split Mathlib.Analysis.BoxIntegral.Partition.Tagged Mathlib.Analysis.Normed.Group.Basic Mathlib.Analysis.Normed.Group.CocompactMap Mathlib.Analysis.Normed.Group.Constructions Mathlib.Analysis.Normed.Group.Int Mathlib.Analysis.Normed.Order.Basic Mathlib.Analysis.Normed.Order.Hom.Basic Mathlib.Analysis.Normed.Order.Hom.Ultra Mathlib.Analysis.NormedSpace.IndicatorFunction Mathlib.Analysis.Oscillation Mathlib.CategoryTheory.Idempotents.SimplicialObject Mathlib.Data.Complex.BigOperators Mathlib.Data.ENNReal.BigOperators Mathlib.Data.EReal.Inv Mathlib.Data.NNReal.Basic Mathlib.InformationTheory.Hamming Mathlib.MeasureTheory.OuterMeasure.Defs Mathlib.NumberTheory.ClassNumber.AdmissibleAbsoluteValue Mathlib.Topology.Algebra.Star.Real Mathlib.Topology.Bornology.Real Mathlib.Topology.Compactness.PseudometrizableLindelof Mathlib.Topology.EMetricSpace.Basic Mathlib.Topology.EMetricSpace.Defs Mathlib.Topology.EMetricSpace.Diam Mathlib.Topology.EMetricSpace.Lipschitz Mathlib.Topology.EMetricSpace.Paracompact Mathlib.Topology.EMetricSpace.Pi Mathlib.Topology.Instances.Int Mathlib.Topology.Instances.Nat Mathlib.Topology.Instances.PNat Mathlib.Topology.MetricSpace.Antilipschitz Mathlib.Topology.MetricSpace.Basic Mathlib.Topology.MetricSpace.Bounded Mathlib.Topology.MetricSpace.Cauchy Mathlib.Topology.MetricSpace.Congruence Mathlib.Topology.MetricSpace.Defs Mathlib.Topology.MetricSpace.Equicontinuity Mathlib.Topology.MetricSpace.Gluing Mathlib.Topology.MetricSpace.Infsep Mathlib.Topology.MetricSpace.Isometry Mathlib.Topology.MetricSpace.MetricSeparated Mathlib.Topology.MetricSpace.ProperSpace.Lemmas Mathlib.Topology.MetricSpace.ProperSpace.Real Mathlib.Topology.MetricSpace.ProperSpace Mathlib.Topology.MetricSpace.Pseudo.Basic Mathlib.Topology.MetricSpace.Pseudo.Constructions Mathlib.Topology.MetricSpace.Pseudo.Defs Mathlib.Topology.MetricSpace.Pseudo.Lemmas Mathlib.Topology.MetricSpace.Pseudo.Pi Mathlib.Topology.MetricSpace.Pseudo.Real Mathlib.Topology.MetricSpace.Sequences Mathlib.Topology.MetricSpace.ShrinkingLemma Mathlib.Topology.MetricSpace.Similarity Mathlib.Topology.MetricSpace.Ultra.Basic Mathlib.Topology.MetricSpace.Ultra.Pi Mathlib.Topology.MetricSpace.Ultra.TotallySeparated Mathlib.Topology.Metrizable.Basic Mathlib.Topology.Metrizable.CompletelyMetrizable Mathlib.Topology.Metrizable.ContinuousMap Mathlib.Topology.Metrizable.Real Mathlib.Topology.Metrizable.Uniformity Mathlib.Topology.Order.Real Mathlib.Topology.UniformSpace.Real	11
78 files Mathlib.Algebra.Module.Card Mathlib.Analysis.Normed.Group.Seminorm Mathlib.CategoryTheory.Noetherian Mathlib.CategoryTheory.Simple Mathlib.CategoryTheory.Sites.Coherent.Basic Mathlib.CategoryTheory.Sites.Coherent.CoherentSheaves Mathlib.CategoryTheory.Sites.Coherent.CoherentTopology Mathlib.CategoryTheory.Sites.Coherent.Comparison Mathlib.CategoryTheory.Sites.Coherent.Equivalence Mathlib.CategoryTheory.Sites.Coherent.ExtensiveColimits Mathlib.CategoryTheory.Sites.Coherent.ExtensiveSheaves Mathlib.CategoryTheory.Sites.Coherent.ExtensiveTopology Mathlib.CategoryTheory.Sites.Coherent.LocallySurjective Mathlib.CategoryTheory.Sites.Coherent.ReflectsPrecoherent Mathlib.CategoryTheory.Sites.Coherent.ReflectsPreregular Mathlib.CategoryTheory.Sites.Coherent.RegularSheaves Mathlib.CategoryTheory.Sites.Coherent.RegularTopology Mathlib.CategoryTheory.Sites.Coherent.SequentialLimit Mathlib.CategoryTheory.Sites.Coherent.SheafComparison Mathlib.CategoryTheory.Sites.ConstantSheaf Mathlib.CategoryTheory.Sites.DenseSubsite.Basic Mathlib.CategoryTheory.Sites.DenseSubsite.InducedTopology Mathlib.CategoryTheory.Sites.DenseSubsite.SheafEquiv Mathlib.CategoryTheory.Sites.EpiMono Mathlib.CategoryTheory.Sites.Equivalence Mathlib.CategoryTheory.Sites.GlobalSections Mathlib.CategoryTheory.Sites.LeftExact Mathlib.CategoryTheory.Sites.LocallyBijective Mathlib.CategoryTheory.Sites.LocallyFullyFaithful Mathlib.CategoryTheory.Sites.LocallyInjective Mathlib.CategoryTheory.Sites.LocallySurjective Mathlib.CategoryTheory.Sites.PreservesLocallyBijective Mathlib.CategoryTheory.Sites.Pullback Mathlib.Combinatorics.Enumerative.IncidenceAlgebra Mathlib.Combinatorics.Pigeonhole Mathlib.Combinatorics.SimpleGraph.IncMatrix Mathlib.Data.DFinsupp.WellFounded Mathlib.Data.ENNReal.Action Mathlib.Data.ENNReal.Basic Mathlib.Data.ENNReal.Holder Mathlib.Data.ENNReal.Inv Mathlib.Data.ENNReal.Lemmas Mathlib.Data.ENNReal.Operations Mathlib.Data.ENNReal.Order Mathlib.Data.ENNReal.Real Mathlib.Data.EReal.Basic Mathlib.Data.EReal.Operations Mathlib.Data.Int.WithZero Mathlib.Data.NNReal.Defs Mathlib.Data.NNReal.Star Mathlib.Data.Real.ConjExponents Mathlib.Data.Real.ENatENNReal Mathlib.Data.Real.EReal Mathlib.Data.Real.Pointwise Mathlib.Data.Setoid.Partition.Card Mathlib.Geometry.RingedSpace.PresheafedSpace.HasColimits Mathlib.Geometry.RingedSpace.SheafedSpace Mathlib.Geometry.RingedSpace.Stalks Mathlib.Topology.Algebra.InfiniteSum.Basic Mathlib.Topology.Algebra.InfiniteSum.Defs Mathlib.Topology.Category.CompHausLike.EffectiveEpi Mathlib.Topology.Sheaves.Alexandrov Mathlib.Topology.Sheaves.Forget Mathlib.Topology.Sheaves.Functors Mathlib.Topology.Sheaves.Limits Mathlib.Topology.Sheaves.LocalPredicate Mathlib.Topology.Sheaves.LocallySurjective Mathlib.Topology.Sheaves.PUnit Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts Mathlib.Topology.Sheaves.SheafCondition.OpensLeCover Mathlib.Topology.Sheaves.SheafCondition.PairwiseIntersections Mathlib.Topology.Sheaves.SheafCondition.Sites Mathlib.Topology.Sheaves.SheafCondition.UniqueGluing Mathlib.Topology.Sheaves.SheafOfFunctions Mathlib.Topology.Sheaves.Sheaf Mathlib.Topology.Sheaves.Sheafify Mathlib.Topology.Sheaves.Skyscraper Mathlib.Topology.Sheaves.Stalks	12
Mathlib.Data.DFinsupp.Lex Mathlib.NumberTheory.EllipticDivisibilitySequence	13
13 files Mathlib.Algebra.Module.BigOperators Mathlib.Algebra.Order.Module.Rat Mathlib.Algebra.QuadraticDiscriminant Mathlib.CategoryTheory.Abelian.Monomorphisms Mathlib.CategoryTheory.Abelian.Subobject Mathlib.CategoryTheory.Idempotents.HomologicalComplex Mathlib.CategoryTheory.Preadditive.Mat Mathlib.CategoryTheory.Sites.Subsheaf Mathlib.Combinatorics.Enumerative.InclusionExclusion Mathlib.Data.Matrix.Mul Mathlib.Data.Matrix.PEquiv Mathlib.LinearAlgebra.Matrix.Integer Mathlib.LinearAlgebra.Matrix.Orthogonal	14
42 files Mathlib.Algebra.BigOperators.Finprod Mathlib.Algebra.BigOperators.GroupWithZero.Action Mathlib.Algebra.Homology.ShortComplex.Abelian Mathlib.CategoryTheory.Abelian.Basic Mathlib.CategoryTheory.Abelian.FunctorCategory Mathlib.CategoryTheory.Adjunction.AdjointFunctorTheorems Mathlib.CategoryTheory.Generator.Sheaf Mathlib.CategoryTheory.Idempotents.Basic Mathlib.CategoryTheory.Idempotents.Biproducts Mathlib.CategoryTheory.Idempotents.FunctorCategories Mathlib.CategoryTheory.Idempotents.FunctorExtension Mathlib.CategoryTheory.Idempotents.KaroubiKaroubi Mathlib.CategoryTheory.Idempotents.Karoubi Mathlib.CategoryTheory.Preadditive.LeftExact Mathlib.CategoryTheory.Preadditive.LiftToFinset Mathlib.CategoryTheory.Sites.Adjunction Mathlib.CategoryTheory.Sites.Canonical Mathlib.CategoryTheory.Sites.CartesianClosed Mathlib.CategoryTheory.Sites.CartesianMonoidal Mathlib.CategoryTheory.Sites.ChosenFiniteProducts Mathlib.CategoryTheory.Sites.CompatiblePlus Mathlib.CategoryTheory.Sites.CompatibleSheafification Mathlib.CategoryTheory.Sites.ConcreteSheafification Mathlib.CategoryTheory.Sites.Continuous Mathlib.CategoryTheory.Sites.CoverLifting Mathlib.CategoryTheory.Sites.CoverPreserving Mathlib.CategoryTheory.Sites.Coverage Mathlib.CategoryTheory.Sites.CoversTop Mathlib.CategoryTheory.Sites.IsSheafOneHypercover Mathlib.CategoryTheory.Sites.Limits Mathlib.CategoryTheory.Sites.Localization Mathlib.CategoryTheory.Sites.Monoidal Mathlib.CategoryTheory.Sites.OneHypercover Mathlib.CategoryTheory.Sites.Over Mathlib.CategoryTheory.Sites.Plus Mathlib.CategoryTheory.Sites.PreservesSheafification Mathlib.CategoryTheory.Sites.SheafHom Mathlib.CategoryTheory.Sites.Sheaf Mathlib.CategoryTheory.Sites.Sheafification Mathlib.CategoryTheory.Sites.Subcanonical Mathlib.CategoryTheory.Sites.Types Mathlib.CategoryTheory.Sites.Whiskering	15
21 files Mathlib.Algebra.Homology.Additive Mathlib.Algebra.Homology.Augment Mathlib.Algebra.Homology.DifferentialObject Mathlib.Algebra.Homology.Double Mathlib.Algebra.Homology.Embedding.Boundary Mathlib.Algebra.Homology.Embedding.Connect Mathlib.Algebra.Homology.Embedding.Restriction Mathlib.Algebra.Homology.Functor Mathlib.Algebra.Homology.HomologicalBicomplex Mathlib.Algebra.Homology.HomologicalComplexBiprod Mathlib.Algebra.Homology.HomologicalComplexLimits Mathlib.Algebra.Homology.HomologicalComplex Mathlib.Algebra.Homology.ImageToKernel Mathlib.Algebra.Homology.Linear Mathlib.Algebra.Homology.Single Mathlib.CategoryTheory.Dialectica.Monoidal Mathlib.CategoryTheory.Generator.Basic Mathlib.CategoryTheory.Generator.HomologicalComplex Mathlib.CategoryTheory.Generator.Presheaf Mathlib.CategoryTheory.Subobject.Lattice Mathlib.CategoryTheory.Subobject.Limits	16
7 files Mathlib.Algebra.Homology.Square Mathlib.Algebra.Order.Rearrangement Mathlib.CategoryTheory.Distributive.Cartesian Mathlib.CategoryTheory.Distributive.Monoidal Mathlib.CategoryTheory.Monoidal.Subcategory Mathlib.CategoryTheory.Shift.Pullback Mathlib.CategoryTheory.Subobject.FactorThru	17
30 files Mathlib.Algebra.Category.Grp.Preadditive Mathlib.Algebra.Category.Grp.ZModuleEquivalence Mathlib.Algebra.Category.ModuleCat.Basic Mathlib.Algebra.Homology.CommSq Mathlib.CategoryTheory.Abelian.NonPreadditive Mathlib.CategoryTheory.Center.Linear Mathlib.CategoryTheory.Center.Localization Mathlib.CategoryTheory.Limits.ConcreteCategory.WithAlgebraicStructures Mathlib.CategoryTheory.Linear.Basic Mathlib.CategoryTheory.Linear.FunctorCategory Mathlib.CategoryTheory.Linear.LinearFunctor Mathlib.CategoryTheory.Localization.Linear Mathlib.CategoryTheory.Localization.Preadditive Mathlib.CategoryTheory.Localization.SmallShiftedHom Mathlib.CategoryTheory.Monoidal.Linear Mathlib.CategoryTheory.Monoidal.Preadditive Mathlib.CategoryTheory.Preadditive.AdditiveFunctor Mathlib.CategoryTheory.Preadditive.Basic Mathlib.CategoryTheory.Preadditive.Biproducts Mathlib.CategoryTheory.Preadditive.EilenbergMoore Mathlib.CategoryTheory.Preadditive.EndoFunctor Mathlib.CategoryTheory.Preadditive.FunctorCategory Mathlib.CategoryTheory.Preadditive.SingleObj Mathlib.CategoryTheory.Quotient.Linear Mathlib.CategoryTheory.Quotient.Preadditive Mathlib.CategoryTheory.Shift.InducedShiftSequence Mathlib.CategoryTheory.Shift.Linear Mathlib.CategoryTheory.Shift.ShiftSequence Mathlib.CategoryTheory.Shift.ShiftedHom Mathlib.CategoryTheory.Triangulated.Rotate	18
Mathlib.Algebra.Order.Module.Pointwise	23
Mathlib.Tactic.LinearCombination Mathlib.Tactic.Polyrith	36
Mathlib.Data.DFinsupp.Order	37
5 files Mathlib.Algebra.Group.EvenFunction Mathlib.Algebra.Order.Algebra Mathlib.Algebra.Order.Module.OrderedSMul Mathlib.Algebra.Order.Monovary Mathlib.Tactic.LinearCombination.Lemmas	38
Mathlib.Algebra.Algebra.Rat Mathlib.Algebra.Order.Module.Algebra	40
Mathlib.Algebra.Module.LinearMap.Rat	41
3 files Mathlib.Algebra.Module.Equiv.Basic Mathlib.Algebra.Module.Rat Mathlib.LinearAlgebra.GeneralLinearGroup	42
Mathlib.Algebra.Module.Hom	46
Mathlib.Algebra.Order.Module.Defs	53
Mathlib.Algebra.NoZeroSMulDivisors.Basic	85
Mathlib.Algebra.Module.End	86

---

Declarations diff

+ AddMonoid.End.ker_id_sub_eq_range
+ AddMonoidHom.ker_coprod_of_disjoint_range
+ AddMonoidHom.ker_prod_ker_le_ker_coprod
+ AddSubgroup.prodEquivOfIsCompl
+ AddSubgroup.sup_eq_range
+ IsIdempotentElem.ker_id_sub_eq_range_cont
+ IsIdempotentElem.range_id_sub_eq_ker_cont
+ idempotentOfClosedCompl
+ is_idempotent_ofClosedCompl
+ ker_id_sub_idempotentOfClosedCompl
+ ker_idempotentOfClosedCompl
+ mem_iff_invariant_ofClosedCompl
+ mem_iff_zero_ofClosedCompl
+ range_id_sub_eq_ker
+ range_id_sub_idempotentOfClosedCompl
+ range_idempotentOfClosedCompl
+ toAddMonoidEnd
++ ker_id_sub_eq_range

You can run this locally as follows

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

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

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

---

No changes to technical debt.

You can run this locally as

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

---

@alreadydone (2024-12-30 00:03 UTC):
Interestingly the norm of P came up in Zulip discussion recently.

---

@YaelDillies (2025-02-10 10:42 UTC):
I think importing Algebra.Group.Idempotent in Algebra.Module.End is fine, but Algebra.Group.Subgroup.Ker seems very not fine. I believe Algebra.Module.End shouldn't know about subgroups at all.

---

@kbuzzard (2025-02-10 10:46 UTC):
At the triage meeting concerns were made about the changes in imports. As you can see from the bot message here, several files are picking up large numbers of new transitive imports because of the imports you're adding in Mathlib/Algebra/Module/End.lean. This is something which people would like to avoid. Can you perhaps put the lemma you've added to this file in a more appropriate place (or even in a new file)? Try using #find_home?

[github-actions]

PR summary a31ee26a74

Import changes exceeding 2%

%	File
+22.16%	Mathlib.Algebra.Module.End
+10.41%	Mathlib.Algebra.Module.Hom

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Algebra.Module.End	388	474	+86 (+22.16%)
Mathlib.Algebra.Module.Hom	442	488	+46 (+10.41%)
Mathlib.Algebra.Module.LinearMap.End	452	453	+1 (+0.22%)

Import changes for all files

Files	Import difference
9 files Mathlib.Algebra.Category.Grp.Kernels Mathlib.Algebra.ModEq Mathlib.Algebra.Module.LinearMap.End Mathlib.Algebra.Module.Submodule.EqLocus Mathlib.Algebra.Module.Submodule.IterateMapComap Mathlib.Algebra.Module.Submodule.Ker Mathlib.Algebra.Module.Submodule.LinearMap Mathlib.Algebra.Module.Submodule.Map Mathlib.GroupTheory.ClassEquation	1
Mathlib.Algebra.Module.Submodule.Invariant	2
3 files Mathlib.Algebra.Module.Submodule.RestrictScalars Mathlib.LinearAlgebra.Matrix.SemiringInverse Mathlib.RingTheory.Localization.Integer	3
21 files Mathlib.Algebra.Order.Antidiag.Nat Mathlib.Algebra.Polynomial.Basic Mathlib.Algebra.Polynomial.Cardinal Mathlib.Algebra.Polynomial.Eval.Algebra Mathlib.Algebra.Polynomial.Eval.Defs Mathlib.Algebra.Polynomial.Monomial Mathlib.Algebra.Ring.CentroidHom Mathlib.Algebra.Squarefree.Basic Mathlib.Algebra.Star.CentroidHom Mathlib.Computability.TMComputable Mathlib.Data.Nat.Squarefree Mathlib.NumberTheory.ArithmeticFunction Mathlib.NumberTheory.MaricaSchoenheim Mathlib.NumberTheory.SmoothNumbers Mathlib.RingTheory.Localization.Defs Mathlib.RingTheory.OreLocalization.Cardinality Mathlib.RingTheory.Radical Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet Mathlib.RingTheory.UniqueFactorizationDomain.Finsupp Mathlib.RingTheory.UniqueFactorizationDomain.GCDMonoid Mathlib.SetTheory.Surreal.Dyadic	4
18 files Mathlib.Algebra.DirectSum.Basic Mathlib.Algebra.DirectSum.Ring Mathlib.Algebra.MonoidAlgebra.Defs Mathlib.Algebra.MonoidAlgebra.Division Mathlib.Algebra.MonoidAlgebra.MapDomain Mathlib.Algebra.MonoidAlgebra.NoZeroDivisors Mathlib.Algebra.SkewMonoidAlgebra.Basic Mathlib.Analysis.Normed.Group.Submodule Mathlib.Data.DFinsupp.Submonoid Mathlib.Dynamics.Flow Mathlib.Dynamics.OmegaLimit Mathlib.LinearAlgebra.Finsupp.LSum Mathlib.RingTheory.Nilpotent.Basic Mathlib.RingTheory.OreLocalization.Ring Mathlib.Topology.Algebra.GroupWithZero Mathlib.Topology.Algebra.Monoid Mathlib.Topology.Algebra.WithZeroTopology Mathlib.Topology.ApproximateUnit	5
19 files Mathlib.Combinatorics.Enumerative.Bell Mathlib.Data.DFinsupp.Interval Mathlib.Data.Finsupp.Antidiagonal Mathlib.Data.Finsupp.Interval Mathlib.Data.Finsupp.MonomialOrder Mathlib.Data.Finsupp.Multiset Mathlib.Data.Finsupp.WellFounded Mathlib.Data.Multiset.Interval Mathlib.Data.Nat.Choose.Factorization Mathlib.Data.Nat.Choose.Multinomial Mathlib.Data.Nat.Factorization.Basic Mathlib.Data.Nat.Factorization.Defs Mathlib.Data.Nat.Factorization.Induction Mathlib.Data.Nat.Factorization.PrimePow Mathlib.Data.Nat.Factorization.Root Mathlib.Logic.Hydra Mathlib.SetTheory.Cardinal.Finsupp Mathlib.SetTheory.Surreal.Multiplication Mathlib.Topology.Algebra.Algebra.Rat	7
7 files Mathlib.Algebra.Order.Floor.Div Mathlib.Analysis.Normed.Group.Subgroup Mathlib.Data.DFinsupp.BigOperators Mathlib.Data.DFinsupp.Multiset Mathlib.Data.Finsupp.Lex Mathlib.Data.Finsupp.Order Mathlib.Data.Finsupp.PWO	8
Mathlib.Analysis.NormedSpace.MStructure	10
70 files Mathlib.Algebra.BigOperators.Balance Mathlib.Algebra.BigOperators.Expect Mathlib.Algebra.Order.BigOperators.Expect Mathlib.AlgebraicTopology.MooreComplex Mathlib.Analysis.BoxIntegral.Box.Basic Mathlib.Analysis.BoxIntegral.Partition.Basic Mathlib.Analysis.BoxIntegral.Partition.Split Mathlib.Analysis.BoxIntegral.Partition.Tagged Mathlib.Analysis.Normed.Group.Basic Mathlib.Analysis.Normed.Group.CocompactMap Mathlib.Analysis.Normed.Group.Constructions Mathlib.Analysis.Normed.Group.Int Mathlib.Analysis.Normed.Order.Basic Mathlib.Analysis.Normed.Order.Hom.Basic Mathlib.Analysis.Normed.Order.Hom.Ultra Mathlib.Analysis.NormedSpace.IndicatorFunction Mathlib.Analysis.Oscillation Mathlib.CategoryTheory.Idempotents.SimplicialObject Mathlib.Data.Complex.BigOperators Mathlib.Data.ENNReal.BigOperators Mathlib.Data.EReal.Inv Mathlib.Data.NNReal.Basic Mathlib.InformationTheory.Hamming Mathlib.MeasureTheory.OuterMeasure.Defs Mathlib.NumberTheory.ClassNumber.AdmissibleAbsoluteValue Mathlib.Topology.Algebra.Star.Real Mathlib.Topology.Bornology.Real Mathlib.Topology.Compactness.PseudometrizableLindelof Mathlib.Topology.EMetricSpace.Basic Mathlib.Topology.EMetricSpace.Defs Mathlib.Topology.EMetricSpace.Diam Mathlib.Topology.EMetricSpace.Lipschitz Mathlib.Topology.EMetricSpace.Paracompact Mathlib.Topology.EMetricSpace.Pi Mathlib.Topology.Instances.Int Mathlib.Topology.Instances.Nat Mathlib.Topology.Instances.PNat Mathlib.Topology.MetricSpace.Antilipschitz Mathlib.Topology.MetricSpace.Basic Mathlib.Topology.MetricSpace.Bounded Mathlib.Topology.MetricSpace.Cauchy Mathlib.Topology.MetricSpace.Congruence Mathlib.Topology.MetricSpace.Defs Mathlib.Topology.MetricSpace.Equicontinuity Mathlib.Topology.MetricSpace.Gluing Mathlib.Topology.MetricSpace.Infsep Mathlib.Topology.MetricSpace.Isometry Mathlib.Topology.MetricSpace.MetricSeparated Mathlib.Topology.MetricSpace.ProperSpace.Lemmas Mathlib.Topology.MetricSpace.ProperSpace.Real Mathlib.Topology.MetricSpace.ProperSpace Mathlib.Topology.MetricSpace.Pseudo.Basic Mathlib.Topology.MetricSpace.Pseudo.Constructions Mathlib.Topology.MetricSpace.Pseudo.Defs Mathlib.Topology.MetricSpace.Pseudo.Lemmas Mathlib.Topology.MetricSpace.Pseudo.Pi Mathlib.Topology.MetricSpace.Pseudo.Real Mathlib.Topology.MetricSpace.Sequences Mathlib.Topology.MetricSpace.ShrinkingLemma Mathlib.Topology.MetricSpace.Similarity Mathlib.Topology.MetricSpace.Ultra.Basic Mathlib.Topology.MetricSpace.Ultra.Pi Mathlib.Topology.MetricSpace.Ultra.TotallySeparated Mathlib.Topology.Metrizable.Basic Mathlib.Topology.Metrizable.CompletelyMetrizable Mathlib.Topology.Metrizable.ContinuousMap Mathlib.Topology.Metrizable.Real Mathlib.Topology.Metrizable.Uniformity Mathlib.Topology.Order.Real Mathlib.Topology.UniformSpace.Real	11
78 files Mathlib.Algebra.Module.Card Mathlib.Analysis.Normed.Group.Seminorm Mathlib.CategoryTheory.Noetherian Mathlib.CategoryTheory.Simple Mathlib.CategoryTheory.Sites.Coherent.Basic Mathlib.CategoryTheory.Sites.Coherent.CoherentSheaves Mathlib.CategoryTheory.Sites.Coherent.CoherentTopology Mathlib.CategoryTheory.Sites.Coherent.Comparison Mathlib.CategoryTheory.Sites.Coherent.Equivalence Mathlib.CategoryTheory.Sites.Coherent.ExtensiveColimits Mathlib.CategoryTheory.Sites.Coherent.ExtensiveSheaves Mathlib.CategoryTheory.Sites.Coherent.ExtensiveTopology Mathlib.CategoryTheory.Sites.Coherent.LocallySurjective Mathlib.CategoryTheory.Sites.Coherent.ReflectsPrecoherent Mathlib.CategoryTheory.Sites.Coherent.ReflectsPreregular Mathlib.CategoryTheory.Sites.Coherent.RegularSheaves Mathlib.CategoryTheory.Sites.Coherent.RegularTopology Mathlib.CategoryTheory.Sites.Coherent.SequentialLimit Mathlib.CategoryTheory.Sites.Coherent.SheafComparison Mathlib.CategoryTheory.Sites.ConstantSheaf Mathlib.CategoryTheory.Sites.DenseSubsite.Basic Mathlib.CategoryTheory.Sites.DenseSubsite.InducedTopology Mathlib.CategoryTheory.Sites.DenseSubsite.SheafEquiv Mathlib.CategoryTheory.Sites.EpiMono Mathlib.CategoryTheory.Sites.Equivalence Mathlib.CategoryTheory.Sites.GlobalSections Mathlib.CategoryTheory.Sites.LeftExact Mathlib.CategoryTheory.Sites.LocallyBijective Mathlib.CategoryTheory.Sites.LocallyFullyFaithful Mathlib.CategoryTheory.Sites.LocallyInjective Mathlib.CategoryTheory.Sites.LocallySurjective Mathlib.CategoryTheory.Sites.PreservesLocallyBijective Mathlib.CategoryTheory.Sites.Pullback Mathlib.Combinatorics.Enumerative.IncidenceAlgebra Mathlib.Combinatorics.Pigeonhole Mathlib.Combinatorics.SimpleGraph.IncMatrix Mathlib.Data.DFinsupp.WellFounded Mathlib.Data.ENNReal.Action Mathlib.Data.ENNReal.Basic Mathlib.Data.ENNReal.Holder Mathlib.Data.ENNReal.Inv Mathlib.Data.ENNReal.Lemmas Mathlib.Data.ENNReal.Operations Mathlib.Data.ENNReal.Order Mathlib.Data.ENNReal.Real Mathlib.Data.EReal.Basic Mathlib.Data.EReal.Operations Mathlib.Data.Int.WithZero Mathlib.Data.NNReal.Defs Mathlib.Data.NNReal.Star Mathlib.Data.Real.ConjExponents Mathlib.Data.Real.ENatENNReal Mathlib.Data.Real.EReal Mathlib.Data.Real.Pointwise Mathlib.Data.Setoid.Partition.Card Mathlib.Geometry.RingedSpace.PresheafedSpace.HasColimits Mathlib.Geometry.RingedSpace.SheafedSpace Mathlib.Geometry.RingedSpace.Stalks Mathlib.Topology.Algebra.InfiniteSum.Basic Mathlib.Topology.Algebra.InfiniteSum.Defs Mathlib.Topology.Category.CompHausLike.EffectiveEpi Mathlib.Topology.Sheaves.Alexandrov Mathlib.Topology.Sheaves.Forget Mathlib.Topology.Sheaves.Functors Mathlib.Topology.Sheaves.Limits Mathlib.Topology.Sheaves.LocalPredicate Mathlib.Topology.Sheaves.LocallySurjective Mathlib.Topology.Sheaves.PUnit Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts Mathlib.Topology.Sheaves.SheafCondition.OpensLeCover Mathlib.Topology.Sheaves.SheafCondition.PairwiseIntersections Mathlib.Topology.Sheaves.SheafCondition.Sites Mathlib.Topology.Sheaves.SheafCondition.UniqueGluing Mathlib.Topology.Sheaves.SheafOfFunctions Mathlib.Topology.Sheaves.Sheaf Mathlib.Topology.Sheaves.Sheafify Mathlib.Topology.Sheaves.Skyscraper Mathlib.Topology.Sheaves.Stalks	12
Mathlib.Data.DFinsupp.Lex Mathlib.NumberTheory.EllipticDivisibilitySequence	13
13 files Mathlib.Algebra.Module.BigOperators Mathlib.Algebra.Order.Module.Rat Mathlib.Algebra.QuadraticDiscriminant Mathlib.CategoryTheory.Abelian.Monomorphisms Mathlib.CategoryTheory.Abelian.Subobject Mathlib.CategoryTheory.Idempotents.HomologicalComplex Mathlib.CategoryTheory.Preadditive.Mat Mathlib.CategoryTheory.Sites.Subsheaf Mathlib.Combinatorics.Enumerative.InclusionExclusion Mathlib.Data.Matrix.Mul Mathlib.Data.Matrix.PEquiv Mathlib.LinearAlgebra.Matrix.Integer Mathlib.LinearAlgebra.Matrix.Orthogonal	14
42 files Mathlib.Algebra.BigOperators.Finprod Mathlib.Algebra.BigOperators.GroupWithZero.Action Mathlib.Algebra.Homology.ShortComplex.Abelian Mathlib.CategoryTheory.Abelian.Basic Mathlib.CategoryTheory.Abelian.FunctorCategory Mathlib.CategoryTheory.Adjunction.AdjointFunctorTheorems Mathlib.CategoryTheory.Generator.Sheaf Mathlib.CategoryTheory.Idempotents.Basic Mathlib.CategoryTheory.Idempotents.Biproducts Mathlib.CategoryTheory.Idempotents.FunctorCategories Mathlib.CategoryTheory.Idempotents.FunctorExtension Mathlib.CategoryTheory.Idempotents.KaroubiKaroubi Mathlib.CategoryTheory.Idempotents.Karoubi Mathlib.CategoryTheory.Preadditive.LeftExact Mathlib.CategoryTheory.Preadditive.LiftToFinset Mathlib.CategoryTheory.Sites.Adjunction Mathlib.CategoryTheory.Sites.Canonical Mathlib.CategoryTheory.Sites.CartesianClosed Mathlib.CategoryTheory.Sites.CartesianMonoidal Mathlib.CategoryTheory.Sites.ChosenFiniteProducts Mathlib.CategoryTheory.Sites.CompatiblePlus Mathlib.CategoryTheory.Sites.CompatibleSheafification Mathlib.CategoryTheory.Sites.ConcreteSheafification Mathlib.CategoryTheory.Sites.Continuous Mathlib.CategoryTheory.Sites.CoverLifting Mathlib.CategoryTheory.Sites.CoverPreserving Mathlib.CategoryTheory.Sites.Coverage Mathlib.CategoryTheory.Sites.CoversTop Mathlib.CategoryTheory.Sites.IsSheafOneHypercover Mathlib.CategoryTheory.Sites.Limits Mathlib.CategoryTheory.Sites.Localization Mathlib.CategoryTheory.Sites.Monoidal Mathlib.CategoryTheory.Sites.OneHypercover Mathlib.CategoryTheory.Sites.Over Mathlib.CategoryTheory.Sites.Plus Mathlib.CategoryTheory.Sites.PreservesSheafification Mathlib.CategoryTheory.Sites.SheafHom Mathlib.CategoryTheory.Sites.Sheaf Mathlib.CategoryTheory.Sites.Sheafification Mathlib.CategoryTheory.Sites.Subcanonical Mathlib.CategoryTheory.Sites.Types Mathlib.CategoryTheory.Sites.Whiskering	15
21 files Mathlib.Algebra.Homology.Additive Mathlib.Algebra.Homology.Augment Mathlib.Algebra.Homology.DifferentialObject Mathlib.Algebra.Homology.Double Mathlib.Algebra.Homology.Embedding.Boundary Mathlib.Algebra.Homology.Embedding.Connect Mathlib.Algebra.Homology.Embedding.Restriction Mathlib.Algebra.Homology.Functor Mathlib.Algebra.Homology.HomologicalBicomplex Mathlib.Algebra.Homology.HomologicalComplexBiprod Mathlib.Algebra.Homology.HomologicalComplexLimits Mathlib.Algebra.Homology.HomologicalComplex Mathlib.Algebra.Homology.ImageToKernel Mathlib.Algebra.Homology.Linear Mathlib.Algebra.Homology.Single Mathlib.CategoryTheory.Dialectica.Monoidal Mathlib.CategoryTheory.Generator.Basic Mathlib.CategoryTheory.Generator.HomologicalComplex Mathlib.CategoryTheory.Generator.Presheaf Mathlib.CategoryTheory.Subobject.Lattice Mathlib.CategoryTheory.Subobject.Limits	16
7 files Mathlib.Algebra.Homology.Square Mathlib.Algebra.Order.Rearrangement Mathlib.CategoryTheory.Distributive.Cartesian Mathlib.CategoryTheory.Distributive.Monoidal Mathlib.CategoryTheory.Monoidal.Subcategory Mathlib.CategoryTheory.Shift.Pullback Mathlib.CategoryTheory.Subobject.FactorThru	17
30 files Mathlib.Algebra.Category.Grp.Preadditive Mathlib.Algebra.Category.Grp.ZModuleEquivalence Mathlib.Algebra.Category.ModuleCat.Basic Mathlib.Algebra.Homology.CommSq Mathlib.CategoryTheory.Abelian.NonPreadditive Mathlib.CategoryTheory.Center.Linear Mathlib.CategoryTheory.Center.Localization Mathlib.CategoryTheory.Limits.ConcreteCategory.WithAlgebraicStructures Mathlib.CategoryTheory.Linear.Basic Mathlib.CategoryTheory.Linear.FunctorCategory Mathlib.CategoryTheory.Linear.LinearFunctor Mathlib.CategoryTheory.Localization.Linear Mathlib.CategoryTheory.Localization.Preadditive Mathlib.CategoryTheory.Localization.SmallShiftedHom Mathlib.CategoryTheory.Monoidal.Linear Mathlib.CategoryTheory.Monoidal.Preadditive Mathlib.CategoryTheory.Preadditive.AdditiveFunctor Mathlib.CategoryTheory.Preadditive.Basic Mathlib.CategoryTheory.Preadditive.Biproducts Mathlib.CategoryTheory.Preadditive.EilenbergMoore Mathlib.CategoryTheory.Preadditive.EndoFunctor Mathlib.CategoryTheory.Preadditive.FunctorCategory Mathlib.CategoryTheory.Preadditive.SingleObj Mathlib.CategoryTheory.Quotient.Linear Mathlib.CategoryTheory.Quotient.Preadditive Mathlib.CategoryTheory.Shift.InducedShiftSequence Mathlib.CategoryTheory.Shift.Linear Mathlib.CategoryTheory.Shift.ShiftSequence Mathlib.CategoryTheory.Shift.ShiftedHom Mathlib.CategoryTheory.Triangulated.Rotate	18
Mathlib.Algebra.Order.Module.Pointwise	23
Mathlib.Tactic.LinearCombination Mathlib.Tactic.Polyrith	36
Mathlib.Algebra.Group.EvenFunction	38
3 files Mathlib.Algebra.Algebra.Rat Mathlib.Algebra.Order.Module.Algebra Mathlib.Data.DFinsupp.Order	40
5 files Mathlib.Algebra.Module.LinearMap.Rat Mathlib.Algebra.Order.Algebra Mathlib.Algebra.Order.Module.OrderedSMul Mathlib.Algebra.Order.Monovary Mathlib.Tactic.LinearCombination.Lemmas	41
3 files Mathlib.Algebra.Module.Equiv.Basic Mathlib.Algebra.Module.Rat Mathlib.LinearAlgebra.GeneralLinearGroup	42
Mathlib.Algebra.Module.Hom	46
Mathlib.Algebra.Order.Module.Field	53
Mathlib.Algebra.Order.Module.Basic Mathlib.Algebra.Order.Module.Defs	65
Mathlib.Algebra.NoZeroSMulDivisors.Basic	85
Mathlib.Algebra.Module.End	86

---

Declarations diff

+ AddMonoid.End.ker_id_sub_eq_range
+ AddMonoidHom.ker_coprod_of_disjoint_range
+ AddMonoidHom.ker_prod_ker_le_ker_coprod
+ AddSubgroup.prodEquivOfIsCompl
+ AddSubgroup.sup_eq_range
+ IsIdempotentElem.ker_id_sub_eq_range_cont
+ IsIdempotentElem.range_id_sub_eq_ker_cont
+ idempotentOfClosedCompl
+ is_idempotent_ofClosedCompl
+ ker_id_sub_idempotentOfClosedCompl
+ ker_idempotentOfClosedCompl
+ mem_iff_invariant_ofClosedCompl
+ mem_iff_zero_ofClosedCompl
+ range_id_sub_eq_ker
+ range_id_sub_idempotentOfClosedCompl
+ range_idempotentOfClosedCompl
+ toAddMonoidEnd
++ ker_id_sub_eq_range

You can run this locally as follows

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

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

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

---

No changes to technical debt.

You can run this locally as

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