Read-back: resolvent_identity

What the statement asserts. For every type $\iota$ that is finite and has decidable equality, and for every pair of arbitrary real square matrices $P, P' \in \mathbb{R}^{\iota \times \iota}$, if the determinant $\det(I - P)$ is a unit of $\mathbb{R}$ and the determinant $\det(I - P')$ is a unit of $\mathbb{R}$ — here $I$ is the identity matrix, and in $\mathbb{R}$ "is a unit" means exactly "is nonzero" — then

an equality of $\iota \times \iota$ real matrices, with the right-hand side associated as $\big((I-P')^{-1}(P'-P)\big)(I-P)^{-1}$ (matrix multiplication is associative, so the grouping is immaterial). Subtraction on both sides is entrywise matrix subtraction.

Binders and hypotheses, in full. The declaration quantifies over: the index type $\iota$ (implicit); the two typeclass assumptions that $\iota$ is a finite type and that equality on $\iota$ is decidable; the two matrices $P$ and $P'$ (explicit); and the two hypotheses $\det(I-P)$ is a unit and $\det(I-P')$ is a unit. There are no other assumptions. In particular nothing requires $P$ or $P'$ to be stochastic, nonnegative, symmetric, substochastic, or related to one another in any way, and no hypothesis about spectral radius, norms, or a discount factor appears.

Constrained vs. free variables in the conclusion. Every variable occurring in the conclusion — $\iota$, $P$, $P'$, and the two instance arguments — is bound by a binder of the theorem; the conclusion contains no free variable and no metavariable. Each of $P$ and $P'$ is constrained by exactly one hypothesis (invertibility of $I-P$, resp. $I-P'$); neither is otherwise restricted.

Joint satisfiability of the hypotheses. The hypotheses are jointly satisfiable and the theorem is therefore not vacuous: taking $P = P' = 0$ gives $\det(I - 0) = 1$, a unit, for both. More generally any pair of matrices with $1$ not an eigenvalue qualifies. Two facts about the reach of the hypotheses are worth recording: (i) when $\iota$ is empty ($n = 0$), $\mathbb{R}^{\iota\times\iota}$ has a single element, every determinant is the empty product $1$, both hypotheses hold automatically, and the conclusion is the trivially true equation between the unique $0\times 0$ matrices; (ii) when $\iota$ is nonempty and $P$ is row-stochastic, every row of $I - P$ sums to $0$, so $(I-P)\mathbf{1} = 0$ and $\det(I - P) = 0$ is not a unit — such $P$ are excluded by the hypothesis, so the statement makes no claim about them.

Behaviour of the inverse on non-invertible arguments. The symbol $(\cdot)^{-1}$ is Mathlib's total matrix inversion: $A^{-1}$ is defined as $\operatorname{Ring.inverse}(\det A) \cdot \operatorname{adj}(A)$, where $\operatorname{Ring.inverse}$ sends a unit to its inverse and sends every non-unit to $0$. Hence for a matrix whose determinant is not invertible (over $\mathbb{R}$: zero), $A^{-1}$ is the zero matrix, not an error and not an undefined value; the operation is total and returns this junk value silently. In this statement that degenerate branch is explicitly ruled out for both inverted matrices: the hypotheses $\operatorname{IsUnit}\det(I-P)$ and $\operatorname{IsUnit}\det(I-P')$ say precisely that $\det(I-P) \neq 0$ and $\det(I-P') \neq 0$, so both $(I-P)^{-1}$ and $(I-P')^{-1}$ are genuine two-sided inverses throughout the conclusion.