diff --git a/Mathlib.lean b/Mathlib.lean
index c9d067db33011c..cd6834e15b91a8 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -5037,6 +5037,7 @@ public import Mathlib.LinearAlgebra.Matrix.HermitianFunctionalCalculus
 public import Mathlib.LinearAlgebra.Matrix.Ideal
 public import Mathlib.LinearAlgebra.Matrix.Integer
 public import Mathlib.LinearAlgebra.Matrix.InvariantBasisNumber
+public import Mathlib.LinearAlgebra.Matrix.InverseLimit
 public import Mathlib.LinearAlgebra.Matrix.Irreducible.Defs
 public import Mathlib.LinearAlgebra.Matrix.IsDiag
 public import Mathlib.LinearAlgebra.Matrix.Kronecker
diff --git a/Mathlib/LinearAlgebra/Matrix/InverseLimit.lean b/Mathlib/LinearAlgebra/Matrix/InverseLimit.lean
new file mode 100644
index 00000000000000..99450a2e45cc32
--- /dev/null
+++ b/Mathlib/LinearAlgebra/Matrix/InverseLimit.lean
@@ -0,0 +1,108 @@
+/-
+Copyright (c) 2026 Allen Hao Zhu. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Allen Hao Zhu
+-/
+module
+
+public import Mathlib.Analysis.Normed.Ring.Units
+public import Mathlib.LinearAlgebra.Matrix.NonsingularInverse
+public import Mathlib.LinearAlgebra.Matrix.Trace
+public import Mathlib.Topology.Instances.Matrix
+
+/-!
+# Regularized matrix inverse: limit as the regularization vanishes
+
+For a square matrix `M` with `det M ≠ 0` over a normed field, the
+**Tikhonov-regularized** expression `(M + lam • 1)⁻¹ * M` converges to the
+identity matrix as the regularization scalar `lam` tends to zero, and
+consequently its trace converges to `tr 1 = Fintype.card d`.
+
+The proof composes existing Mathlib infrastructure:
+
+* `NormedRing.inverse_continuousAt` — continuity of `Ring.inverse` at any unit
+  of a normed ring with summable geometric series (automatic for a normed
+  field),
+* `continuousAt_matrix_inv` — continuity of matrix inversion at any matrix
+  whose determinant is a unit (from `Mathlib.Topology.Instances.Matrix`),
+* `Matrix.nonsing_inv_mul` — the algebraic identity `M⁻¹ * M = 1` at a
+  matrix with unit determinant,
+* `Continuous.matrix_trace` — continuity of the matrix trace.
+
+## Main results
+
+* `Matrix.regularizedInv_mul_tendsto_one`:
+  `(M + lam • 1)⁻¹ * M ⟶ 1` as `lam → 0`, for `M` with `det M ≠ 0`.
+* `Matrix.trace_regularizedInv_mul_tendsto`:
+  `tr ((M + lam • 1)⁻¹ * M) ⟶ tr 1` as `lam → 0`.
+* `Matrix.trace_regularizedInv_mul_tendsto_card`: the specialization stating
+  that the limit equals `(Fintype.card d : R)`.
+
+These lemmas are useful in matrix-regularization limit arguments arising in
+numerical linear algebra (Tikhonov-regularized least squares, ridge
+regression) and in statistics.
+-/
+
+@[expose] public section
+
+namespace Matrix
+
+open Filter Topology
+
+variable {d R : Type*} [Fintype d] [DecidableEq d] [NormedField R]
+
+/-- For a square matrix `M` with nonzero determinant over a normed field, the
+regularized inverse `(M + lam • 1)⁻¹ * M` tends to the identity matrix as the
+scalar `lam` tends to zero. -/
+theorem regularizedInv_mul_tendsto_one
+    (M : Matrix d d R) (hM : M.det ≠ 0) :
+    Tendsto (fun lam : R => (M + lam • (1 : Matrix d d R))⁻¹ * M)
+      (𝓝 0) (𝓝 (1 : Matrix d d R)) := by
+  -- The perturbation `lam ↦ M + lam • 1` is continuous.
+  have h_add : Continuous (fun lam : R => M + lam • (1 : Matrix d d R)) :=
+    continuous_const.add (continuous_id.smul continuous_const)
+  -- `Ring.inverse` is continuous at the (nonzero) determinant of `M`.
+  have h_det_unit : IsUnit M.det := isUnit_iff_ne_zero.mpr hM
+  have h_ring_inv : ContinuousAt Ring.inverse M.det := by
+    have := NormedRing.inverse_continuousAt h_det_unit.unit
+    simpa [IsUnit.unit_spec] using this
+  -- Hence `Inv.inv` on matrices is continuous at `M`.
+  have h_mat_inv : ContinuousAt (Inv.inv : Matrix d d R → Matrix d d R) M :=
+    continuousAt_matrix_inv M h_ring_inv
+  -- The perturbation evaluates to `M` at `lam = 0`, so the composition
+  -- `lam ↦ (M + lam • 1)⁻¹` is continuous at `0`.
+  have h_g0 : M + (0 : R) • (1 : Matrix d d R) = M := by simp
+  have h_inv_comp :
+      ContinuousAt (fun lam : R => (M + lam • (1 : Matrix d d R))⁻¹) 0 :=
+    h_mat_inv.comp_of_eq h_add.continuousAt h_g0
+  -- Multiply on the right by the constant `M`.
+  have h_mul :
+      ContinuousAt (fun lam : R => (M + lam • (1 : Matrix d d R))⁻¹ * M) 0 :=
+    h_inv_comp.mul continuousAt_const
+  -- Identify the limit value `M⁻¹ * M` with `1` via `Matrix.nonsing_inv_mul`.
+  have h_value :
+      (M + (0 : R) • (1 : Matrix d d R))⁻¹ * M = (1 : Matrix d d R) := by
+    rw [h_g0]; exact Matrix.nonsing_inv_mul M h_det_unit
+  have h_tendsto := h_mul.tendsto
+  rw [h_value] at h_tendsto
+  exact h_tendsto
+
+/-- Trace version of `regularizedInv_mul_tendsto_one`: the trace of
+`(M + lam • 1)⁻¹ * M` tends to `tr 1` as `lam → 0`. -/
+theorem trace_regularizedInv_mul_tendsto
+    (M : Matrix d d R) (hM : M.det ≠ 0) :
+    Tendsto (fun lam : R => ((M + lam • (1 : Matrix d d R))⁻¹ * M).trace)
+      (𝓝 0) (𝓝 ((1 : Matrix d d R).trace)) :=
+  (continuous_id.matrix_trace.tendsto _).comp
+    (regularizedInv_mul_tendsto_one M hM)
+
+/-- Specialization of `trace_regularizedInv_mul_tendsto` via `Matrix.trace_one`:
+the trace of the regularized inverse tends to `(Fintype.card d : R)`. -/
+theorem trace_regularizedInv_mul_tendsto_card
+    (M : Matrix d d R) (hM : M.det ≠ 0) :
+    Tendsto (fun lam : R => ((M + lam • (1 : Matrix d d R))⁻¹ * M).trace)
+      (𝓝 0) (𝓝 ((Fintype.card d : ℕ) : R)) := by
+  have h := trace_regularizedInv_mul_tendsto M hM
+  simpa [Matrix.trace_one] using h
+
+end Matrix