[proofplan] We apply the Leibniz formula and show that any permutation $\sigma \in S_n$ (where $n = k + \ell$) contributing a non-zero term must preserve the block partition: $\sigma$ maps $\{1, \dots, k\}$ to itself and $\{k+1, \dots, n\}$ to itself. This is forced by the zero block in the lower-left corner. The sum then factors into independent sums over $S_k$ and $S_\ell$, yielding $(\det A)(\det B)$. [/proofplan] [step:Set up the block structure and the Leibniz formula] Write $n = k + \ell$ and let $M = \begin{pmatrix} A & C \\ \mathbf{0} & B \end{pmatrix} \in \mathrm{Mat}_n(\mathbb{F})$. Partition the index set as $\{1, \dots, k\}$ (corresponding to block $A$) and $\{k+1, \dots, n\}$ (corresponding to block $B$). The block structure means $M_{ij} = 0$ for $i > k$ and $j \leq k$ (the lower-left block is zero). By the Leibniz formula: \begin{align*} \det M = \sum_{\sigma \in S_n} \varepsilon(\sigma) \prod_{i=1}^n M_{i,\sigma(i)}. \end{align*} [/step] [step:Show that contributing permutations must preserve the block partition] [claim:Block Preserving Permutations] If $\sigma \in S_n$ satisfies $\prod_{i=1}^n M_{i,\sigma(i)} \neq 0$, then $\sigma$ maps $\{1, \dots, k\}$ to $\{1, \dots, k\}$ and $\{k+1, \dots, n\}$ to $\{k+1, \dots, n\}$. [/claim] [proof] For the product $\prod_{i=1}^n M_{i,\sigma(i)}$ to be non-zero, each factor $M_{i,\sigma(i)}$ must be non-zero. For $i \in \{k+1, \dots, n\}$: the lower-left block is zero, so $M_{i,j} = 0$ for all $j \leq k$. Hence $M_{i,\sigma(i)} \neq 0$ requires $\sigma(i) > k$. This shows $\sigma$ maps $\{k+1, \dots, n\}$ into $\{k+1, \dots, n\}$. Since $\sigma$ is a bijection on $\{1, \dots, n\}$ and maps $\{k+1, \dots, n\}$ into itself, it must also map $\{1, \dots, k\}$ into $\{1, \dots, k\}$ (by cardinality: $\sigma$ restricted to each block is an injection between finite sets of equal size, hence a bijection). [/proof] [guided] The zero block is the key structural constraint. For $i > k$ (rows in the lower portion), the only non-zero entries are in columns $j > k$ (the $B$ block). So any permutation $\sigma$ that sends some $i > k$ to a column $j \leq k$ would produce a zero factor $M_{i,j} = 0$, killing the entire product. Therefore every contributing permutation maps $\{k+1, \dots, n\}$ into $\{k+1, \dots, n\}$. Since $\sigma$ is a bijection on $\{1, \dots, n\}$ and the image of $\{k+1, \dots, n\}$ stays within $\{k+1, \dots, n\}$ (a set of the same finite cardinality), $\sigma$ restricted to $\{k+1, \dots, n\}$ is a bijection. The complement $\{1, \dots, k\}$ is then also mapped bijectively to itself. [/guided] [/step] [step:Factor the Leibniz sum into the product $(\det A)(\det B)$] By the claim, the only contributing permutations decompose as $\sigma = (\sigma_1, \sigma_2)$ where $\sigma_1 \in S_k$ acts on $\{1, \dots, k\}$ and $\sigma_2 \in S_\ell$ acts on $\{k+1, \dots, n\}$. Since $\sigma_1$ and $\sigma_2$ act on disjoint index sets, $\varepsilon(\sigma) = \varepsilon(\sigma_1)\varepsilon(\sigma_2)$. Moreover, $M_{i,\sigma_1(i)} = A_{i,\sigma_1(i)}$ for $i \leq k$ and $M_{i,\sigma_2(i)} = B_{i-k,\sigma_2(i)-k}$ for $i > k$. Therefore: \begin{align*} \det M &= \sum_{\substack{\sigma_1 \in S_k \\ \sigma_2 \in S_\ell}} \varepsilon(\sigma_1)\varepsilon(\sigma_2) \prod_{i=1}^k A_{i,\sigma_1(i)} \prod_{i=k+1}^{n} B_{i-k,\,\sigma_2(i)-k} \\ &= \left(\sum_{\sigma_1 \in S_k} \varepsilon(\sigma_1) \prod_{i=1}^k A_{i,\sigma_1(i)}\right) \left(\sum_{\sigma_2 \in S_\ell} \varepsilon(\sigma_2) \prod_{j=1}^\ell B_{j,\sigma_2'(j)}\right) \\ &= (\det A)(\det B), \end{align*} where in the second factor we substituted $j = i - k$ and wrote $\sigma_2'(j) = \sigma_2(j + k) - k \in S_\ell$. The result for block lower triangular matrices $\begin{pmatrix} A & \mathbf{0} \\ D & B \end{pmatrix}$ follows by the same argument applied to the zero block in the upper-right corner, or equivalently by transposing and using $\det M^\top = \det M$. [/step]