feat(LinearAlgebra/Matrix/SchurComplement): rank-one determinant formula det(1 - φ•c) = 1 - φ c

[tobias-weiss-ai-xr]

Adds LinearMap.det_one_sub_smulRight: for a linear functional φ : M →ₗ[R] R and a vector c : M over a nontrivial commutative ring, the determinant of the rank-one endomorphism x ↦ φ x • c shifted by the identity is 1 - φ c:

theorem det_one_sub_smulRight [Nontrivial R] [Module.Free R M] [Module.Finite R M]
    (φ : M →ₗ[R] R) (c : M) :
    LinearMap.det ((1 : M →ₗ[R] M) - φ.smulRight c) = 1 - φ c

This lifts the rank-one specialization of the Weinstein–Aronszajn identity (Matrix.det_one_sub_mul_comm) to endomorphisms of a finite free module via LinearMap.det_toMatrix.

• The new import Mathlib.LinearAlgebra.Determinant into SchurComplement.lean is acyclic (Determinant does not import SchurComplement).
• Verified to build warning-free under the pinned toolchain.

[github-actions]

Welcome new contributor!

Thank you for contributing to Mathlib! If you haven't done so already, please review our contribution guidelines, as well as the style guide and naming conventions. In particular, we kindly remind contributors that we have guidelines regarding the use of AI when making pull requests.

We use a review queue to manage reviews. If your PR does not appear there, it is probably because it is not successfully building (i.e., it doesn't have a green checkmark), has the awaiting-author tag, or another reason described in the Lifecycle of a PR. The review dashboard has a dedicated webpage which shows whether your PR is on the review queue, and (if not), why.

If you haven't already done so, please come to Zulip and join the Lean community.
Thank you again for joining our community.

[github-actions]

PR summary a24b42113a

Import changes exceeding 2%

%	File
+8.22%	Mathlib.LinearAlgebra.Matrix.SchurComplement

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.LinearAlgebra.Matrix.SchurComplement	1643	1778	+135 (+8.22%)

Import changes for all files

Files	Import difference
Mathlib.RingTheory.Trace.Defs	2
Mathlib.Algebra.Lie.Classical Mathlib.LinearAlgebra.Matrix.Cartan.Realisation	6
12 files Mathlib.LinearAlgebra.RootSystem.BaseExists Mathlib.LinearAlgebra.RootSystem.Base Mathlib.LinearAlgebra.RootSystem.Basic Mathlib.LinearAlgebra.RootSystem.Chain Mathlib.LinearAlgebra.RootSystem.Finite.G2 Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Lemmas Mathlib.LinearAlgebra.RootSystem.Hom Mathlib.LinearAlgebra.RootSystem.Irreducible Mathlib.LinearAlgebra.RootSystem.RootPairingCat Mathlib.LinearAlgebra.RootSystem.WeylGroup	7
Mathlib.RingTheory.Flat.Rank	12
5 files Mathlib.LinearAlgebra.RootSystem.BaseChange Mathlib.LinearAlgebra.RootSystem.Finite.CanonicalBilinear Mathlib.LinearAlgebra.RootSystem.IsValuedIn Mathlib.LinearAlgebra.RootSystem.Reduced Mathlib.LinearAlgebra.RootSystem.RootPositive	16
Mathlib.RingTheory.Depth.Rees Mathlib.RingTheory.PicardGroup	17
12 files Mathlib.NumberTheory.DirichletCharacter.Orthogonality Mathlib.NumberTheory.MulChar.Duality Mathlib.RingTheory.Etale.Locus Mathlib.RingTheory.Flat.LocallyFree Mathlib.RingTheory.Grassmannian Mathlib.RingTheory.RegularLocalRing.Defs Mathlib.RingTheory.RegularLocalRing.Polynomial Mathlib.RingTheory.RingHom.Smooth Mathlib.RingTheory.Smooth.Local Mathlib.RingTheory.Smooth.Locus Mathlib.RingTheory.Smooth.Quotient Mathlib.RingTheory.Spectrum.Prime.FreeLocus	29
Mathlib.RingTheory.RingHom.Unramified Mathlib.RingTheory.Unramified.Locus	30
8 files Mathlib.GroupTheory.FiniteAbelian.Duality Mathlib.RingTheory.DedekindDomain.Dvr Mathlib.RingTheory.DedekindDomain.Instances Mathlib.RingTheory.DedekindDomain.PID Mathlib.RingTheory.Flat.TorsionFree Mathlib.RingTheory.KrullDimension.Regular Mathlib.RingTheory.LocalProperties.Semilocal Mathlib.RingTheory.RingHom.QuasiFinite	31
6 files Mathlib.RingTheory.Etale.Basic Mathlib.RingTheory.Etale.Kaehler Mathlib.RingTheory.Etale.Pi Mathlib.RingTheory.Smooth.AdicCompletion Mathlib.RingTheory.Smooth.Basic Mathlib.RingTheory.Smooth.Pi	32
10 files Mathlib.NumberTheory.LocalField.Basic Mathlib.NumberTheory.Padics.LocalField Mathlib.RingTheory.DiscreteValuationRing.TFAE Mathlib.RingTheory.QuasiFinite.Basic Mathlib.RingTheory.QuasiFinite.Weakly Mathlib.RingTheory.Unramified.Basic Mathlib.RingTheory.Unramified.Finite Mathlib.RingTheory.Unramified.Pi Mathlib.RingTheory.Valuation.Discrete.RankOne Mathlib.Topology.Algebra.Valued.LocallyCompact	33
13 files Mathlib.Algebra.Module.DedekindDomain Mathlib.Algebra.Module.PID Mathlib.GroupTheory.FiniteAbelian.Basic Mathlib.RingTheory.AdicCompletion.Noetherian Mathlib.RingTheory.HopkinsLevitzki Mathlib.RingTheory.Ideal.KrullsHeightTheorem Mathlib.RingTheory.Ideal.UFD Mathlib.RingTheory.Jacobson.Artinian Mathlib.RingTheory.KrullDimension.Polynomial Mathlib.RingTheory.OrderOfVanishing.Basic Mathlib.RingTheory.Spectrum.Prime.LTSeries Mathlib.RingTheory.Valuation.Discrete.Basic Mathlib.Topology.Algebra.Valued.WithZeroMulInt	34
Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema	36
Mathlib.Algebra.Polynomial.Module.FiniteDimensional Mathlib.NumberTheory.Padics.ValuativeRel	39
Mathlib.Topology.Algebra.Valued.NormedValued	40
Mathlib.NumberTheory.RamificationInertia.Ramification	42
Mathlib.Analysis.AbsoluteValue.Equivalence Mathlib.NumberTheory.Ostrowski	43
3 files Mathlib.FieldTheory.Normal.Basic Mathlib.FieldTheory.Normal.Closure Mathlib.NumberTheory.Niven	45
8 files Mathlib.AlgebraicGeometry.AlgebraicCycle.Basic Mathlib.FieldTheory.Extension Mathlib.FieldTheory.FinTrdeg Mathlib.FieldTheory.IntermediateField.Adjoin.Basic Mathlib.FieldTheory.Minpoly.ConjRootClass Mathlib.FieldTheory.Minpoly.IsConjRoot Mathlib.FieldTheory.Relrank Mathlib.RingTheory.AlgebraicIndependent.RankAndCardinality	46
61 files Mathlib.Algebra.DirectSum.LinearMap Mathlib.AlgebraicGeometry.AffineScheme Mathlib.AlgebraicGeometry.Cover.Directed Mathlib.AlgebraicGeometry.Cover.Over Mathlib.AlgebraicGeometry.Cover.QuasiCompact Mathlib.AlgebraicGeometry.Cover.Sigma Mathlib.AlgebraicGeometry.EffectiveEpi Mathlib.AlgebraicGeometry.Fiber Mathlib.AlgebraicGeometry.FunctionField Mathlib.AlgebraicGeometry.Geometrically.Basic Mathlib.AlgebraicGeometry.GluingOneHypercover Mathlib.AlgebraicGeometry.Group.Affine Mathlib.AlgebraicGeometry.IdealSheaf.Basic Mathlib.AlgebraicGeometry.IdealSheaf.Functorial Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme Mathlib.AlgebraicGeometry.LimitsOver Mathlib.AlgebraicGeometry.Limits 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.FiniteType Mathlib.AlgebraicGeometry.Morphisms.Finite Mathlib.AlgebraicGeometry.Morphisms.Flat 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.QuasiSeparated Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties Mathlib.AlgebraicGeometry.Morphisms.SchemeTheoreticallyDominant Mathlib.AlgebraicGeometry.Morphisms.Separated Mathlib.AlgebraicGeometry.Morphisms.SurjectiveOnStalks Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap Mathlib.AlgebraicGeometry.Morphisms.UniversallyClosed Mathlib.AlgebraicGeometry.PointsPi Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Functor Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Proper Mathlib.AlgebraicGeometry.Properties Mathlib.AlgebraicGeometry.PullbackCarrier Mathlib.AlgebraicGeometry.Pullbacks Mathlib.AlgebraicGeometry.QuasiAffine Mathlib.AlgebraicGeometry.ResidueField Mathlib.AlgebraicGeometry.Sites.Affine Mathlib.AlgebraicGeometry.Sites.BigZariski Mathlib.AlgebraicGeometry.Sites.Pretopology Mathlib.AlgebraicGeometry.Sites.QuasiCompact Mathlib.AlgebraicGeometry.Sites.Representability Mathlib.AlgebraicGeometry.Sites.SheafQuasiCompact Mathlib.AlgebraicGeometry.Sites.Small Mathlib.AlgebraicGeometry.Stalk Mathlib.AlgebraicGeometry.ValuativeCriterion	47
32 files Mathlib.Algebra.Category.ModuleCat.Descent Mathlib.Algebra.Category.Ring.EqualizerPushout Mathlib.Algebra.Category.Ring.Under.Limits Mathlib.Algebra.Category.Ring.Under.Property Mathlib.AlgebraicGeometry.Cover.MorphismProperty Mathlib.AlgebraicGeometry.Cover.Open Mathlib.AlgebraicGeometry.GammaSpecAdjunction Mathlib.AlgebraicGeometry.Gluing Mathlib.AlgebraicGeometry.Modules.Presheaf Mathlib.AlgebraicGeometry.Modules.Sheaf Mathlib.AlgebraicGeometry.OpenImmersion Mathlib.AlgebraicGeometry.Over Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme Mathlib.AlgebraicGeometry.Restrict Mathlib.AlgebraicGeometry.Scheme Mathlib.AlgebraicGeometry.Sites.MorphismProperty Mathlib.AlgebraicGeometry.Spec Mathlib.LinearAlgebra.PID Mathlib.LinearAlgebra.SymplecticGroup Mathlib.LinearAlgebra.Trace Mathlib.RingTheory.Algebraic.StronglyTranscendental Mathlib.RingTheory.Finiteness.Descent Mathlib.RingTheory.Flat.FaithfullyFlat.Descent Mathlib.RingTheory.KrullDimension.Module Mathlib.RingTheory.LocalIso Mathlib.RingTheory.LocalProperties.IntegrallyClosed Mathlib.RingTheory.RingHom.FaithfullyFlat Mathlib.RingTheory.RingHom.FinitePresentation Mathlib.RingTheory.RingHom.Flat Mathlib.RingTheory.RingHom.Integral Mathlib.RingTheory.Spectrum.Prime.Module Mathlib.RingTheory.TensorProduct.IncludeLeftSubRight	48
8 files Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed Mathlib.NumberTheory.FLT.Polynomial Mathlib.NumberTheory.KummerDedekind Mathlib.RingTheory.IntegralClosure.GoingDown Mathlib.RingTheory.Invariant.Profinite Mathlib.RingTheory.IsAdjoinRoot Mathlib.RingTheory.Polynomial.GaussLemma Mathlib.Topology.Algebra.Valued.ValuedField	49
48 files Mathlib.Algebra.GCDMonoid.IntegrallyClosed Mathlib.Algebra.Order.Ring.StandardPart Mathlib.AlgebraicGeometry.StructureSheaf Mathlib.Analysis.Real.Hyperreal Mathlib.RingTheory.ClassGroup.Basic Mathlib.RingTheory.ClassGroup.ExtendedHom Mathlib.RingTheory.ClassGroup Mathlib.RingTheory.Conductor Mathlib.RingTheory.DedekindDomain.Basic Mathlib.RingTheory.DedekindDomain.Ideal.Basic Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas Mathlib.RingTheory.Finiteness.FinitePresentationLocal Mathlib.RingTheory.Flat.FaithfullyFlat.Algebra Mathlib.RingTheory.FractionalIdeal.Extended Mathlib.RingTheory.Ideal.GoingDown Mathlib.RingTheory.Ideal.GoingUp Mathlib.RingTheory.Ideal.HasGoingUp Mathlib.RingTheory.Ideal.Height Mathlib.RingTheory.IntegralClosure.IntegrallyClosed Mathlib.RingTheory.Invariant.Basic Mathlib.RingTheory.IsGaloisGroup.Basic Mathlib.RingTheory.Jacobson.Ring Mathlib.RingTheory.KrullDimension.LocalRing Mathlib.RingTheory.KrullDimension.PID Mathlib.RingTheory.KrullDimension.Zero Mathlib.RingTheory.LocalRing.Length Mathlib.RingTheory.LocalRing.ResidueField.Fiber Mathlib.RingTheory.LocalRing.ResidueField.Instances Mathlib.RingTheory.Localization.Pi Mathlib.RingTheory.Polynomial.IsIntegral Mathlib.RingTheory.Polynomial.RationalRoot Mathlib.RingTheory.Spectrum.Maximal.Topology Mathlib.RingTheory.Spectrum.Prime.ConstructibleSet Mathlib.RingTheory.Spectrum.Prime.IsOpenComapC Mathlib.RingTheory.Spectrum.Prime.Jacobson Mathlib.RingTheory.Spectrum.Prime.Noetherian Mathlib.RingTheory.Spectrum.Prime.TensorProduct Mathlib.RingTheory.Spectrum.Prime.Topology Mathlib.RingTheory.UniqueFactorizationDomain.ClassGroup Mathlib.RingTheory.Valuation.AlgebraInstances Mathlib.RingTheory.Valuation.Extension Mathlib.RingTheory.Valuation.Integral Mathlib.RingTheory.Valuation.LocalSubring Mathlib.RingTheory.Valuation.RamificationGroup Mathlib.RingTheory.Valuation.ValuationSubring Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology Mathlib.Topology.Algebra.Valued.ValuationTopology Mathlib.Topology.Algebra.Valued.ValuativeRel	50
3 files Mathlib.Analysis.Normed.Field.WithAbs Mathlib.FieldTheory.SplittingField.Construction Mathlib.FieldTheory.SplittingField.IsSplittingField	52
17 files Mathlib.Algebra.Polynomial.Bivariate Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula Mathlib.FieldTheory.Fixed Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra Mathlib.FieldTheory.IntermediateField.Algebraic Mathlib.FieldTheory.Normal.Defs Mathlib.FieldTheory.Separable Mathlib.RingTheory.Adjoin.Polynomial.Bivariate Mathlib.RingTheory.AlgebraicIndependent.Adjoin Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis Mathlib.RingTheory.Derivation.MapCoeffs Mathlib.RingTheory.Polynomial.SeparableDegree	53
Mathlib.LinearAlgebra.Eigenspace.Minpoly	54
Mathlib.RingTheory.Adjoin.PowerBasis Mathlib.RingTheory.Finiteness.ModuleFinitePresentation	55
12 files Mathlib.FieldTheory.Minpoly.Field Mathlib.FieldTheory.RatFunc.Basic Mathlib.LinearAlgebra.AnnihilatingPolynomial Mathlib.LinearAlgebra.Matrix.Charpoly.Minpoly Mathlib.RingTheory.Adjoin.Field Mathlib.RingTheory.AdjoinRoot Mathlib.RingTheory.Algebraic.Denominator Mathlib.RingTheory.Algebraic.Integral Mathlib.RingTheory.Localization.Away.AdjoinRoot Mathlib.RingTheory.Localization.Integral Mathlib.RingTheory.PowerBasis Mathlib.RingTheory.Valuation.Minpoly	56
Mathlib.FieldTheory.IntermediateField.ExtendRight	57
Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic Mathlib.RingTheory.NoetherNormalization	60
Mathlib.LinearAlgebra.Matrix.Charpoly.Univ	66
Mathlib.RingTheory.IntegralClosure.IsIntegral.AlmostIntegral	77
Mathlib.FieldTheory.Minpoly.Finite	79
Mathlib.RingTheory.IntegralClosure.Algebra.Basic Mathlib.RingTheory.IntegralClosure.Algebra.Ideal	84
Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff Mathlib.LinearAlgebra.Matrix.Charpoly.LinearMap	85
Mathlib.LinearAlgebra.Matrix.SchurComplement	135

---

Declarations diff (regex)

+ det_one_sub_smulRight

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

• +1 new declarations
• −0 removed declarations

+LinearMap.det_one_sub_smulRight

---

No changes to strong technical debt.
No changes to weak technical debt.

Current commit a24b42113a
Reference commit 8d52ea9a14

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

[tobias-weiss-ai-xr]

Rebased onto current master (the previous base predated the cache storage-layout migration, which broke the CI cache step). Built warning-free locally with the pinned toolchain. Requesting the topic label t-linear-algebra.