feat(RingTheory): lemmas on finiteness of LinearMap and Module.End

[alreadydone]

---

One less lemma than #24012, but with the advantage of not depending on #23963.

• depends on: [Merged by Bors] - chore: automatically additivize IsScalarTower #24115

[github-actions]

PR summary 875ca65160

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.RingTheory.Finiteness.Basic	984	989	+5 (+0.51%)

Import changes for all files

Files	Import difference
176 files Mathlib.Algebra.Algebra.Subalgebra.Rank Mathlib.Algebra.AlgebraicCard Mathlib.Algebra.Category.Grp.EnoughInjectives Mathlib.Algebra.Category.Grp.Injective Mathlib.Algebra.Category.Grp.LargeColimits Mathlib.Algebra.Category.Grp.Ulift Mathlib.Algebra.Category.ModuleCat.EnoughInjectives Mathlib.Algebra.Category.ModuleCat.Free Mathlib.Algebra.Category.Ring.Constructions Mathlib.Algebra.Category.Ring.Epi Mathlib.Algebra.Category.Ring.FinitePresentation Mathlib.Algebra.Category.Ring.Instances Mathlib.Algebra.Category.Ring.Under.Basic Mathlib.Algebra.CharP.LocalRing Mathlib.Algebra.CharP.MixedCharZero Mathlib.Algebra.DualQuaternion Mathlib.Algebra.Homology.LocalCohomology Mathlib.Algebra.LinearRecurrence Mathlib.Algebra.Module.CharacterModule Mathlib.Algebra.Module.FinitePresentation Mathlib.Algebra.Module.Presentation.Finite Mathlib.Algebra.Module.SpanRank Mathlib.Algebra.MvPolynomial.Funext Mathlib.Algebra.Polynomial.Expand Mathlib.Algebra.QuaternionBasis Mathlib.Algebra.Quaternion Mathlib.AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf Mathlib.CategoryTheory.Preadditive.HomOrthogonal Mathlib.Data.Nat.Choose.Lucas Mathlib.Data.Real.GoldenRatio Mathlib.Data.Real.Irrational Mathlib.Data.ZMod.QuotientRing Mathlib.FieldTheory.Minpoly.Basic Mathlib.FieldTheory.MvRatFunc.Rank Mathlib.FieldTheory.Tower Mathlib.Geometry.RingedSpace.LocallyRingedSpace.HasColimits Mathlib.Geometry.RingedSpace.LocallyRingedSpace.ResidueField Mathlib.Geometry.RingedSpace.LocallyRingedSpace Mathlib.Geometry.RingedSpace.OpenImmersion Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing Mathlib.GroupTheory.FreeGroup.GeneratorEquiv Mathlib.LinearAlgebra.Dimension.Constructions Mathlib.LinearAlgebra.Dimension.Finite Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition Mathlib.LinearAlgebra.Dimension.Free Mathlib.LinearAlgebra.Dimension.RankNullity Mathlib.LinearAlgebra.Dimension.StrongRankCondition Mathlib.LinearAlgebra.FreeAlgebra Mathlib.LinearAlgebra.FreeModule.Finite.Quotient Mathlib.LinearAlgebra.FreeModule.IdealQuotient Mathlib.LinearAlgebra.FreeModule.Int Mathlib.LinearAlgebra.FreeModule.ModN Mathlib.LinearAlgebra.FreeModule.PID Mathlib.LinearAlgebra.FreeModule.StrongRankCondition Mathlib.LinearAlgebra.InvariantBasisNumber Mathlib.LinearAlgebra.LinearDisjoint Mathlib.LinearAlgebra.Matrix.Adjugate Mathlib.LinearAlgebra.Matrix.FixedDetMatrices Mathlib.LinearAlgebra.Matrix.Ideal Mathlib.LinearAlgebra.Matrix.InvariantBasisNumber Mathlib.LinearAlgebra.Matrix.Nondegenerate Mathlib.LinearAlgebra.Matrix.ProjectiveSpecialLinearGroup Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup Mathlib.LinearAlgebra.TensorAlgebra.Basis Mathlib.LinearAlgebra.TensorProduct.Vanishing Mathlib.NumberTheory.BernoulliPolynomials Mathlib.NumberTheory.Bernoulli Mathlib.NumberTheory.DiophantineApproximation.Basic Mathlib.NumberTheory.DiophantineApproximation.ContinuedFractions Mathlib.NumberTheory.FLT.Polynomial Mathlib.NumberTheory.ModularForms.CongruenceSubgroups Mathlib.NumberTheory.Pell Mathlib.NumberTheory.Rayleigh Mathlib.RingTheory.AdicCompletion.Basic Mathlib.RingTheory.AdicCompletion.LocalRing Mathlib.RingTheory.AdicCompletion.Noetherian Mathlib.RingTheory.Adjoin.Dimension Mathlib.RingTheory.Adjoin.FG Mathlib.RingTheory.Adjoin.Tower Mathlib.RingTheory.Algebraic.Basic Mathlib.RingTheory.Algebraic.MvPolynomial Mathlib.RingTheory.AlgebraicIndependent.Transcendental Mathlib.RingTheory.DiscreteValuationRing.Basic Mathlib.RingTheory.DualNumber Mathlib.RingTheory.EssentialFiniteness Mathlib.RingTheory.Filtration Mathlib.RingTheory.FinitePresentation Mathlib.RingTheory.FiniteStability Mathlib.RingTheory.FiniteType Mathlib.RingTheory.Finiteness.Ideal Mathlib.RingTheory.Finiteness.Quotient Mathlib.RingTheory.Finiteness.Small Mathlib.RingTheory.Flat.Basic Mathlib.RingTheory.Flat.CategoryTheory Mathlib.RingTheory.Flat.Equalizer Mathlib.RingTheory.Flat.EquationalCriterion Mathlib.RingTheory.Flat.FaithfullyFlat.Algebra Mathlib.RingTheory.Flat.FaithfullyFlat.Basic Mathlib.RingTheory.Flat.Localization Mathlib.RingTheory.Flat.Stability Mathlib.RingTheory.FractionalIdeal.Basic Mathlib.RingTheory.FractionalIdeal.Extended Mathlib.RingTheory.FractionalIdeal.Operations Mathlib.RingTheory.GradedAlgebra.FiniteType Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization Mathlib.RingTheory.GradedAlgebra.Noetherian Mathlib.RingTheory.Henselian Mathlib.RingTheory.Ideal.AssociatedPrime Mathlib.RingTheory.Ideal.MinimalPrime.Localization Mathlib.RingTheory.Ideal.Quotient.Index Mathlib.RingTheory.Ideal.Quotient.Noetherian Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic Mathlib.RingTheory.Jacobson.Ideal Mathlib.RingTheory.Jacobson.Polynomial Mathlib.RingTheory.Jacobson.Radical Mathlib.RingTheory.KrullDimension.Basic Mathlib.RingTheory.KrullDimension.Field Mathlib.RingTheory.Lasker Mathlib.RingTheory.LocalProperties.Basic Mathlib.RingTheory.LocalProperties.Exactness Mathlib.RingTheory.LocalProperties.Projective Mathlib.RingTheory.LocalProperties.Reduced Mathlib.RingTheory.LocalProperties.Submodule Mathlib.RingTheory.LocalRing.LocalSubring Mathlib.RingTheory.LocalRing.MaximalIdeal.Basic Mathlib.RingTheory.LocalRing.NonLocalRing Mathlib.RingTheory.LocalRing.ResidueField.Basic Mathlib.RingTheory.LocalRing.ResidueField.Defs Mathlib.RingTheory.LocalRing.ResidueField.Ideal Mathlib.RingTheory.LocalRing.RingHom.Basic Mathlib.RingTheory.Localization.AsSubring Mathlib.RingTheory.Localization.AtPrime Mathlib.RingTheory.Localization.Away.Lemmas Mathlib.RingTheory.Localization.Finiteness Mathlib.RingTheory.Localization.Free Mathlib.RingTheory.Localization.InvSubmonoid Mathlib.RingTheory.Localization.LocalizationLocalization Mathlib.RingTheory.Localization.Submodule Mathlib.RingTheory.MvPolynomial Mathlib.RingTheory.Nakayama Mathlib.RingTheory.Noetherian.Basic Mathlib.RingTheory.Noetherian.Nilpotent Mathlib.RingTheory.Noetherian.Orzech Mathlib.RingTheory.Polynomial.Basic Mathlib.RingTheory.Polynomial.Eisenstein.Basic Mathlib.RingTheory.Polynomial.Eisenstein.Criterion Mathlib.RingTheory.Polynomial.Eisenstein.Distinguished Mathlib.RingTheory.Polynomial.Quotient Mathlib.RingTheory.Polynomial.UniqueFactorization Mathlib.RingTheory.PowerSeries.Derivative Mathlib.RingTheory.PowerSeries.Inverse Mathlib.RingTheory.ReesAlgebra Mathlib.RingTheory.RingHom.FiniteType Mathlib.RingTheory.RingHom.Finite Mathlib.RingTheory.RingHom.Injective Mathlib.RingTheory.RingHom.Locally Mathlib.RingTheory.RingHom.Surjective Mathlib.RingTheory.RingHomProperties Mathlib.RingTheory.SimpleRing.Matrix Mathlib.RingTheory.Spectrum.Maximal.Localization Mathlib.RingTheory.Spectrum.Prime.Basic Mathlib.RingTheory.Spectrum.Prime.RingHom Mathlib.RingTheory.Support Mathlib.RingTheory.SurjectiveOnStalks Mathlib.RingTheory.TensorProduct.Finite Mathlib.RingTheory.Valuation.RamificationGroup Mathlib.RingTheory.Valuation.ValuationSubring Mathlib.RingTheory.ZMod Mathlib.Tactic.ReduceModChar Mathlib.Topology.Algebra.IsOpenUnits Mathlib.Topology.Algebra.SeparationQuotient.FiniteDimensional Mathlib.Topology.Algebra.Valued.ValuationTopology Mathlib.Topology.Algebra.Valued.ValuedField Mathlib.Topology.Instances.AddCircle.DenseSubgroup Mathlib.Topology.Instances.Irrational Mathlib.Topology.Instances.RatLemmas	1
4 files Mathlib.Data.ZMod.Coprime Mathlib.NumberTheory.FLT.Four Mathlib.NumberTheory.PythagoreanTriples Mathlib.RingTheory.Finiteness.Finsupp	2
61 files Mathlib.Algebra.Azumaya.Basic Mathlib.Algebra.Azumaya.Matrix Mathlib.Algebra.Category.BialgebraCat.Basic Mathlib.Algebra.Category.BialgebraCat.Monoidal Mathlib.Algebra.Category.CoalgebraCat.Basic Mathlib.Algebra.Category.CoalgebraCat.ComonEquivalence Mathlib.Algebra.Category.CoalgebraCat.Monoidal Mathlib.Algebra.Category.HopfAlgebraCat.Basic Mathlib.Algebra.Category.HopfAlgebraCat.Monoidal Mathlib.Algebra.Colimit.TensorProduct Mathlib.Algebra.CubicDiscriminant Mathlib.Algebra.Polynomial.Degree.CardPowDegree Mathlib.Algebra.Polynomial.Derivation Mathlib.Algebra.Polynomial.FieldDivision Mathlib.Algebra.Polynomial.Module.AEval Mathlib.Algebra.Polynomial.Module.Basic Mathlib.Algebra.Polynomial.SpecificDegree Mathlib.Algebra.Polynomial.Splits Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass Mathlib.FieldTheory.RatFunc.Basic Mathlib.LinearAlgebra.TensorProduct.Finiteness Mathlib.NumberTheory.Dioph Mathlib.NumberTheory.FLT.Basic Mathlib.NumberTheory.FLT.MasonStothers Mathlib.NumberTheory.PellMatiyasevic Mathlib.NumberTheory.Zsqrtd.Basic Mathlib.NumberTheory.Zsqrtd.GaussianInt Mathlib.NumberTheory.Zsqrtd.ToReal Mathlib.RingTheory.AlgebraicIndependent.Basic Mathlib.RingTheory.Bezout Mathlib.RingTheory.Bialgebra.Basic Mathlib.RingTheory.Bialgebra.Equiv Mathlib.RingTheory.Bialgebra.Hom Mathlib.RingTheory.Bialgebra.MonoidAlgebra Mathlib.RingTheory.Bialgebra.TensorProduct Mathlib.RingTheory.Coalgebra.Basic Mathlib.RingTheory.Coalgebra.Equiv Mathlib.RingTheory.Coalgebra.Hom Mathlib.RingTheory.Coalgebra.MonoidAlgebra Mathlib.RingTheory.Coalgebra.TensorProduct Mathlib.RingTheory.EuclideanDomain Mathlib.RingTheory.Finiteness.Projective Mathlib.RingTheory.Finiteness.Subalgebra Mathlib.RingTheory.HopfAlgebra.Basic Mathlib.RingTheory.HopfAlgebra.MonoidAlgebra Mathlib.RingTheory.HopfAlgebra.TensorProduct Mathlib.RingTheory.Ideal.IsPrincipal Mathlib.RingTheory.Int.Basic Mathlib.RingTheory.MvPolynomial.Basic Mathlib.RingTheory.Noetherian.UniqueFactorizationDomain Mathlib.RingTheory.Polynomial.Content Mathlib.RingTheory.Polynomial.Radical Mathlib.RingTheory.Polynomial.SmallDegreeVieta Mathlib.RingTheory.Polynomial.Vieta Mathlib.RingTheory.PrincipalIdealDomainOfPrime Mathlib.RingTheory.PrincipalIdealDomain Mathlib.RingTheory.Valuation.Archimedean Mathlib.RingTheory.Valuation.ValuationRing	4
9 files Mathlib.Algebra.Colimit.Finiteness Mathlib.LinearAlgebra.FreeModule.Finite.Basic Mathlib.RingTheory.Finiteness.Basic Mathlib.RingTheory.Finiteness.Cardinality Mathlib.RingTheory.Finiteness.Lattice Mathlib.RingTheory.Noetherian.Defs Mathlib.RingTheory.Noetherian.Filter Mathlib.RingTheory.OrzechProperty Mathlib.Topology.Algebra.Module.Compact	5

---

Declarations diff

+ instance (priority := 50) [SMul T M] [SMulMemClass S T M] [SMulCommClass T R M] :
+ instance (priority := 50) [SMulCommClass M N α] : SMulCommClass M N s
+ instance (priority := 50) [SMulCommClass N M α] : SMulCommClass N M s
+ instance [Module R₀ M] [SMulCommClass R R₀ M] [SMul R₀ R] [IsScalarTower R₀ R M]
+ instance [Module R₀ P] [SMulCommClass R R₀ P] [Module.Finite R₀ (M →ₗ[R] P)] :
+ instance [Module.Finite R M] : Module.Finite R Mᵐᵒᵖ := equiv (MulOpposite.opLinearEquiv R)
+ of_isComplemented_codomain
+ of_isComplemented_domain
+ surjective_comp_linearProjOfIsCompl
+ surjective_comp_subtype_of_isComplemented

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

[mathlib4-dependent-issues-bot]

This PR/issue depends on:

• [Merged by Bors] - chore: automatically additivize IsScalarTower #24115
  By Dependent Issues (🤖). Happy coding!

[leanprover-community-mathlib4-bot]

!bench

[leanprover-bot]

Here are the benchmark results for commit 875ca65.
There were no significant changes against commit d4fc037.

[github-actions]

File	Instructions	%
build	+16.598⬝10⁹	(+0.01%)
Mathlib.GroupTheory.GroupAction.SubMulAction	+4.551⬝10⁹	(+18.01%)

2 files, Instructions +2.0⬝10⁹

File	Instructions	%
Mathlib.RingTheory.Finiteness.Basic	+2.732⬝10⁹	(+14.93%)
Mathlib.RingTheory.SimpleModule.Basic	+2.674⬝10⁹	(+3.82%)

2 files, Instructions +1.0⬝10⁹

File	Instructions	%
Mathlib.LinearAlgebra.Projection	+1.586⬝10⁹	(+2.65%)
Mathlib.LinearAlgebra.BilinearMap	+1.491⬝10⁹	(+2.26%)

CI run