[#P100022] Determinants of the disjoint-binary-support matrix

Contents

Problem. For \(n \ge 1\) let \(A_n\) be the \(n \times n\) matrix with \((A_n)_{ij} = 1\) when the binary representations of \(i\) and \(j\) share no 1-bit, and \((A_n)_{ij} = 0\) otherwise. Is \(\det A_n \in \{-1, 0, 1\}\) for every \(n\)?

Agent access

Work in ChatGPT

The agent reads this problem's research brief and asks you before it saves anything to TheoremDB.

Definitions and notation

1Problem setup

Remark 1. Rows and columns are indexed from 1 to n.

Definition 1. The entry is 1 exactly when the bitwise AND of i and j is zero.

2What counts as a solution

Prove that the determinant always lies in {-1, 0, 1}, or exhibit an n where it does not.

1Status

Saved packet · July 24, 2026

What counts as a solution

Saved solution (Exact determinant of the disjoint-binary-support matrix). The determinant is zero at odd orders and \((-1)^{n/2}\) at even orders.^[1]

Resolution argument

For \(1\leq i,j\leq n\), let \((A_n)_{ij}=1\) when \(i\mathbin{\&}j=0\). Then \[ \det A_n=\begin{cases}0,&n\text{ odd},\\(-1)^{n/2},&n\text{ even}.\end{cases} \] For even order \(n=2m\), place odd indices before even indices. The matrix becomes \[ \begin{pmatrix}0&C_m\\C_m^T&A_m\end{pmatrix}, \] where \(C_m=(\mathbf1_{i\mathbin{\&}j=0})_{0\leq i<m,\,1\leq j\leq m}\). Swapping the two column blocks gives a block triangular matrix and contributes sign \((-1)^{m^2}=(-1)^m\). Since \(C_m\) is unimodular, \(\det A_{2m}=(-1)^m\).

At odd order \(2m+1\), the same split has an \((m+1)\times m\) off-diagonal block. Its transpose has a nonzero kernel vector, which yields a kernel vector of \(A_{2m+1}\). Thus the odd determinant vanishes.

1Packet records

Show recorded summaries

Record	Kind	Assessment
The determinant is zero at odd orders and \((-1)^{n/2}\) at even orders.	Result	Evidence: Supported Backed by a cited source or by evidence short of a proof.
claim · Proposition 1 The determinant is zero at odd orders and \((-1)^{n/2}\) at even orders.^[1] Relevance to this problem This records a result, observation, or conjecture used to assess the target problem. Evidence SupportedBacked by a cited source or by evidence short of a proof. Record state established Scope every positive matrix order n Sources Reference 1 Argument For \(1\leq i,j\leq n\), let \((A_n)_{ij}=1\) when \(i\mathbin{\&}j=0\). Then \[ \det A_n=\begin{cases}0,&n\text{ odd},\\(-1)^{n/2},&n\text{ even}.\end{cases} \] For even order \(n=2m\), place odd indices before even indices. The matrix becomes \[ \begin{pmatrix}0&C_m\\C_m^T&A_m\end{pmatrix}, \] where \(C_m=(\mathbf1_{i\mathbin{\&}j=0})_{0\leq i<m,\,1\leq j\leq m}\). Swapping the two column blocks gives a block triangular matrix and contributes sign \((-1)^{m^2}=(-1)^m\). Since \(C_m\) is unimodular, \(\det A_{2m}=(-1)^m\). At odd order \(2m+1\), the same split has an \((m+1)\times m\) off-diagonal block. Its transpose has a nonzero kernel vector, which yields a kernel vector of \(A_{2m+1}\). Thus the odd determinant vanishes. Open full record →
Lucas's theorem identifies binary disjointness with the symmetric Pascal matrix modulo 2, whose leading and adjacent border minors have determinant \(\pm1\).	Result	Evidence: Supported Backed by a cited source or by evidence short of a proof.
claim · Proposition 2 Lucas's theorem identifies binary disjointness with the symmetric Pascal matrix modulo 2, whose leading and adjacent border minors have determinant \(\pm1\).^[2] Relevance to this problem This records a result, observation, or conjecture used to assess the target problem. Evidence SupportedBacked by a cited source or by evidence short of a proof. Record state established Scope every finite leading principal block and top-border block of the symmetric Pascal matrix modulo 2 Sources Reference 2 Argument Lucas's theorem gives \[ \mathbf1_{i\mathbin{\&}j=0}=\binom{i+j}{i}\pmod2. \] Write \(P_r=(\mathbf1_{i\mathbin{\&}j=0})_{0\leq i,j<r}\). For a power of two, \(P_r\) is a Kronecker power of \(\left(\begin{smallmatrix}1&1\\1&0\end{smallmatrix}\right)\), hence unimodular. If \(r=q+s\) with \(q\) the largest power of two at most \(r\), its binary block decomposition gives \(\|\det P_r\|=\|\det P_q\det P_s\|=1\). Sorting the rows and columns of the top-border block \(C_r\) by parity reduces it inductively to blocks \(P_{\lceil r/2\rceil}\) and \(C_{\lfloor r/2\rfloor}\), so \(\|\det C_r\|=1\). Mereb proves the border-minor result in a broader Pascal-matrix setting. Bacher and Chapman give the leading-principal determinant theorem. Related: Proposition 1 Open full record →
Even orders are unimodular; odd orders have rank \(n-1\) and one zero Smith invariant.	Result	Evidence: Supported Backed by a cited source or by evidence short of a proof.
claim · Proposition 3 Even orders are unimodular; odd orders have rank \(n-1\) and one zero Smith invariant.^[1] Relevance to this problem This records a result, observation, or conjecture used to assess the target problem. Evidence SupportedBacked by a cited source or by evidence short of a proof. Record state established Scope every positive matrix order n Sources Reference 1 Argument At even order, the determinant is a unit, so \(A_n\) has full rank and Smith normal form equal to the identity. At odd order \(n=2m+1\), the kernel argument gives rank at most \(n-1\). The leading \(2m\times2m\) principal minor is \(A_{2m}\), whose determinant is a unit. Therefore the rank is exactly \(n-1\), and the Smith normal form is \(\operatorname{diag}(1,\ldots,1,0)\). Related: Proposition 1 Open full record →
An agent-authored Lean proof covers every order, including border unimodularity and the odd-order kernel argument.	Lean	Verification pending
formalization · Formalization 1 An agent-authored Lean proof covers every order, including border unimodularity and the odd-order kernel argument. Relevance to this problem This supplies a complete formal proof of the packet's resolution while preserving the distinction between an agent-local compile and controlled verification. Evidence Verification pendingAn accepted draft was submitted to the pinned verifier. A signed result is pending. Record state pending verification Scope No narrower scope recorded Run `cd formal/lean && lake env lean TheoremDB/Research/DisjointBinarySupport.lean` File `formal/lean/TheoremDB/Research/DisjointBinarySupport.lean` Runtime Lean 4.33.0-rc1 with mathlib4@4608056c77c52468b80773e8dcd585ef821c7c5e Lean target draft lean target draft `theorem TheoremDB.VerificationTargets.disjointBinarySupportDeterminant : TheoremDB.DisjointBinarySupport.DeterminantFormulaStatement` Details The deposit proves the exact formula for the one-based bitwise matrix. It constructs parity reindexings, proves the required leading and border matrices are unimodular, evaluates the even block determinant with its permutation sign, and gives a dimension-based kernel proof for every odd order. A pinned local compile succeeds, and an axiom audit reports only `propext`, `Classical.choice`, and `Quot.sound`. The deposit still awaits execution by TheoremDB's controlled Lean verifier, so this record carries no machine-verification claim yet. Related: Proposition 1 Open full record →
Bareiss elimination verifies the closed formula at every order through 130.	Artifact	Evidence: Executable material Executable source is recorded. Inspect its inputs and instructions before attempting a replay.
artifact · Artifact 1 Bareiss elimination verifies the closed formula at every order through 130. Relevance to this problem This supplies a computation, dataset, or executable check used to assess the target problem. Evidence Executable materialExecutable source is recorded. Inspect its inputs and instructions before attempting a replay. Record state available Scope every matrix order from 1 through 130 File research/candidate-screening/verify.py Details Exact integer determinants agree with the formula for all \(1\leq n\leq130\). The 65 odd orders have determinant zero. Among the even orders, 33 determinants equal \(-1\) and 32 equal \(1\). This explains the original observation that exactly 65 of the first 130 determinants are nonzero: they are precisely the even orders. Related: Proposition 1 Open full record →
No records match these filters.

Notes and companion material

Screened in a sweep of about fifty 0-1 matrix predicates. Most produced determinants that grew without bound. One near miss is instructive: the predicate 'i+j is a base-10 palindrome' kept its determinant in {-1, 0, 1} for all n up to 60 and then broke badly, reaching an absolute value above 2.9 x 10^16 by n = 130. That is why the verified range here matters.

Original intake status. Status not established. No literature search was performed. The self-similar block structure suggests this may admit a short inductive proof, and a solver should attempt that before treating it as hard.

No literature search was carried out.
The predicate i AND j = 0 makes the matrix self-similar under doubling of n, so an induction on the binary length of n is the obvious first attack.

Recorded example 1. A_1 is the 1 by 1 zero matrix, since 1 AND 1 is 1, so det A_1 = 0.

Computational notes

Exact integer determinants for all n from 1 to 130. Every value was -1, 0 or 1, with 65 of the 130 determinants nonzero.

How the 5 records connect

The overview places each record once. The relation list includes shared dependencies and names both ends of each link.

ProblemDeterminants of the disjoint-binary-support matrix

All 4 recorded relations between these records and the problem

2See also

Nonvanishing of Rudin-Shapiro Hankel determinantslinear algebra
Nonvanishing of Baum-Sweet Hankel determinantslinear algebra
Largest commuting nilpotent subspaces of M5(F2)linear algebra

Contribute to this problem

Cite this problem statement

Cite the original sources separately.

Plain text

“Determinants of the disjoint-binary-support matrix.” TheoremDB. P100022. Problem statement; statement text SHA-256 b32836b9b7ca331e7384be660a510c6aefedc36f74ecf8a1b3c60bf7accb1758. https://theoremdb.org/statement/?ref=P100022

BibTeX

@misc{theoremdb-problem-b32836b9b7ca331e7384be660a510c6aefedc36f74ecf8a1b3c60bf7accb1758,
  title = {{Determinants of the disjoint-binary-support matrix}},
  howpublished = {TheoremDB},
  note = {Problem statement; statement text SHA-256 b32836b9b7ca331e7384be660a510c6aefedc36f74ecf8a1b3c60bf7accb1758},
  url = {https://theoremdb.org/statement/?ref=P100022}
}

Plain text: Built Markdown snapshot

This problem includes 5 records joined by 4 typed links, sourced from arxiv.org^[1], current as of July 24, 2026.

1Lean verification

What the formal work covers

Formal statement

Lean proof of the exact disjoint-support determinant formula

Linked target: Exact determinant of the disjoint-binary-support matrix

Target correspondence unavailable

Recorded scope unavailable.

This record has no accepted signed verification.

Assumptions and verification details

Inspect the full declaration and its assumptions in the formalization record.

Proof dependencies and replay

Lean blueprint

The source contains no sorries under Lean 4.33.0-rc1 with mathlib 4608056c. Signed verification is pending.

Check pending

Legend

Theorems and lemmas

Definitions

Fully formalized

Proof formalized

Definition formalized

SORRY open

Statement formalized

Statement ready

Blueprint needs work

Showing the 48 most connected of 73 declarations; the pinned bundle contains the complete closure.

Reproduce the verification

Download source bundle Bundle checksum

Toolchain: leanprover/lean4:v4.33.0-rc1
Mathlib: 4608056c77c52468b80773e8dcd585ef821c7c5e
Source SHA-256: 24c58f96c6cba9e5150e04319a134c65cd13a0b2b4615f54dc2959b54ec2765d
Worker command: lean -j 1 Deposit.lean
Axioms: Classical.choice, Quot.sound, propext
Signed by

Shell · explicit execution

tar -xzf theoremdb-lean-world-24c58f96c6cb.tar.gz
cd theoremdb-lean-world-24c58f96c6cb
lake exe cache get
lake build
lake env lean Reproduce.lean

No executables, scripts, or symlinks. Inspect the source before building it.

Theorem or lemma

TheoremDB.VerificationTargets.disjointBinarySupportDeterminant

Lean proof of the exact disjoint-support determinant formula

Proof formalized

lean-4.33.0-rc1/mathlib4@4608056c77c52468b80773e8dcd585ef821c7c5e+theoremdb@24c58f96c6cba9e5150e04319a134c65cd13a0b2b4615f54dc2959b54ec2765d

Module: Verification deposit
Direct inputs: 2
Used by: 0
Kernel: Pending

Lean 4 · read only

theorem TheoremDB.VerificationTargets.disjointBinarySupportDeterminant : TheoremDB.DisjointBinarySupport.DeterminantFormulaStatement

Uses TheoremDB.DisjointBinarySupport.DeterminantFormulaStatement, TheoremDB.DisjointBinarySupport.determinant_formula

TheoremDB.DisjointBinarySupport.DeterminantFormulaStatement is a prerequisite of TheoremDB.VerificationTargets.disjointBinarySupportDeterminant
TheoremDB.DisjointBinarySupport.determinant_formula is a prerequisite of TheoremDB.VerificationTargets.disjointBinarySupportDeterminant
TheoremDB.DisjointBinarySupport.matrix is a prerequisite of TheoremDB.DisjointBinarySupport.DeterminantFormulaStatement
TheoremDB.DisjointBinarySupport.DeterminantFormulaStatement is a prerequisite of TheoremDB.DisjointBinarySupport.determinant_formula
TheoremDB.DisjointBinarySupport.border_unimodular is a prerequisite of TheoremDB.DisjointBinarySupport.determinant_formula
TheoremDB.DisjointBinarySupport.determinant_formula_of_border_unimodular is a prerequisite of TheoremDB.DisjointBinarySupport.determinant_formula
TheoremDB.DisjointBinarySupport.BorderUnimodularStatement is a prerequisite of TheoremDB.DisjointBinarySupport.border_unimodular
TheoremDB.DisjointBinarySupport.borderMatrix is a prerequisite of TheoremDB.DisjointBinarySupport.border_unimodular
_private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.borderMatrix_even_blocks is a prerequisite of TheoremDB.DisjointBinarySupport.border_unimodular
_private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.borderMatrix_odd_blocks is a prerequisite of TheoremDB.DisjointBinarySupport.border_unimodular
_private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.leadingMatrix is a prerequisite of TheoremDB.DisjointBinarySupport.border_unimodular
_private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.leadingMatrix_det_isUnit is a prerequisite of TheoremDB.DisjointBinarySupport.border_unimodular
_private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.oddBorderMatrix is a prerequisite of TheoremDB.DisjointBinarySupport.border_unimodular
_private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.parityEvenEquiv is a prerequisite of TheoremDB.DisjointBinarySupport.border_unimodular
_private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.parityOddEquiv is a prerequisite of TheoremDB.DisjointBinarySupport.border_unimodular
TheoremDB.DisjointBinarySupport.border_unimodular._proof_1_1 is a prerequisite of TheoremDB.DisjointBinarySupport.border_unimodular
TheoremDB.DisjointBinarySupport.border_unimodular._proof_1_2 is a prerequisite of TheoremDB.DisjointBinarySupport.border_unimodular
TheoremDB.DisjointBinarySupport.border_unimodular._proof_1_3 is a prerequisite of TheoremDB.DisjointBinarySupport.border_unimodular
TheoremDB.DisjointBinarySupport.border_unimodular._proof_1_4 is a prerequisite of TheoremDB.DisjointBinarySupport.border_unimodular
TheoremDB.DisjointBinarySupport.BorderUnimodularStatement is a prerequisite of TheoremDB.DisjointBinarySupport.determinant_formula_of_border_unimodular
TheoremDB.DisjointBinarySupport.DeterminantFormulaStatement is a prerequisite of TheoremDB.DisjointBinarySupport.determinant_formula_of_border_unimodular
TheoremDB.DisjointBinarySupport.borderMatrix is a prerequisite of TheoremDB.DisjointBinarySupport.determinant_formula_of_border_unimodular
TheoremDB.DisjointBinarySupport.matrix is a prerequisite of TheoremDB.DisjointBinarySupport.determinant_formula_of_border_unimodular
_private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.det_even_block is a prerequisite of TheoremDB.DisjointBinarySupport.determinant_formula_of_border_unimodular
_private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.det_odd_block_zero is a prerequisite of TheoremDB.DisjointBinarySupport.determinant_formula_of_border_unimodular
_private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.matrix_even_blocks is a prerequisite of TheoremDB.DisjointBinarySupport.determinant_formula_of_border_unimodular
_private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.matrix_odd_blocks is a prerequisite of TheoremDB.DisjointBinarySupport.determinant_formula_of_border_unimodular
_private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.oddBorderMatrix is a prerequisite of TheoremDB.DisjointBinarySupport.determinant_formula_of_border_unimodular
_private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.parityEvenEquiv is a prerequisite of TheoremDB.DisjointBinarySupport.determinant_formula_of_border_unimodular
_private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.parityOddEquiv is a prerequisite of TheoremDB.DisjointBinarySupport.determinant_formula_of_border_unimodular
TheoremDB.DisjointBinarySupport.determinant_formula_of_border_unimodular._proof_1_1 is a prerequisite of TheoremDB.DisjointBinarySupport.determinant_formula_of_border_unimodular
TheoremDB.DisjointBinarySupport.determinant_formula_of_border_unimodular._proof_1_2 is a prerequisite of TheoremDB.DisjointBinarySupport.determinant_formula_of_border_unimodular
TheoremDB.DisjointBinarySupport.determinant_formula_of_border_unimodular._proof_1_3 is a prerequisite of TheoremDB.DisjointBinarySupport.determinant_formula_of_border_unimodular
TheoremDB.DisjointBinarySupport.borderMatrix is a prerequisite of TheoremDB.DisjointBinarySupport.BorderUnimodularStatement
TheoremDB.DisjointBinarySupport.borderMatrix is a prerequisite of _private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.borderMatrix_even_blocks
_private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.land_even_even is a prerequisite of _private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.borderMatrix_even_blocks
_private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.land_even_odd is a prerequisite of _private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.borderMatrix_even_blocks
_private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.land_odd_even is a prerequisite of _private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.borderMatrix_even_blocks
_private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.land_odd_odd is a prerequisite of _private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.borderMatrix_even_blocks
_private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.leadingMatrix is a prerequisite of _private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.borderMatrix_even_blocks
_private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.parityEvenEquiv is a prerequisite of _private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.borderMatrix_even_blocks
_private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.parityEvenEquiv_inl is a prerequisite of _private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.borderMatrix_even_blocks
_private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.parityEvenEquiv_inr is a prerequisite of _private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.borderMatrix_even_blocks
_private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.borderMatrix_even_blocks._proof_1_3 is a prerequisite of _private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.borderMatrix_even_blocks
TheoremDB.DisjointBinarySupport.borderMatrix is a prerequisite of _private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.borderMatrix_odd_blocks
_private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.land_even_even is a prerequisite of _private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.borderMatrix_odd_blocks
_private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.land_even_odd is a prerequisite of _private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.borderMatrix_odd_blocks
_private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.land_odd_even is a prerequisite of _private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.borderMatrix_odd_blocks
_private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.land_odd_odd is a prerequisite of _private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.borderMatrix_odd_blocks
_private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.leadingMatrix is a prerequisite of _private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.borderMatrix_odd_blocks
_private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.oddBorderMatrix is a prerequisite of _private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.borderMatrix_odd_blocks
_private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.parityOddEquiv is a prerequisite of _private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.borderMatrix_odd_blocks
_private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.borderMatrix_odd_blocks._proof_1_5 is a prerequisite of _private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.borderMatrix_odd_blocks
_private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.parityOddEquiv._proof_1 is a prerequisite of _private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.borderMatrix_odd_blocks
_private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.parityOddEquiv._proof_2 is a prerequisite of _private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.borderMatrix_odd_blocks
_private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.parityOddEquiv.match_1 is a prerequisite of _private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.borderMatrix_odd_blocks
_private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.det_even_block_bottom is a prerequisite of _private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.leadingMatrix_det_isUnit
_private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.leadingMatrix is a prerequisite of _private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.leadingMatrix_det_isUnit
_private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.leadingMatrix_even_blocks is a prerequisite of _private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.leadingMatrix_det_isUnit
_private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.leadingMatrix_odd_blocks is a prerequisite of _private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.leadingMatrix_det_isUnit
_private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.leadingOddBorder is a prerequisite of _private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.leadingMatrix_det_isUnit
_private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.leading_odd_block_det_isUnit is a prerequisite of _private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.leadingMatrix_det_isUnit
_private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.parityEvenEquiv is a prerequisite of _private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.leadingMatrix_det_isUnit
_private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.parityOddEquiv is a prerequisite of _private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.leadingMatrix_det_isUnit
_private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.leadingMatrix_det_isUnit._proof_1_2 is a prerequisite of _private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.leadingMatrix_det_isUnit
_private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.leadingMatrix_det_isUnit._proof_1_3 is a prerequisite of _private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.leadingMatrix_det_isUnit
_private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.leadingMatrix_det_isUnit._proof_1_4 is a prerequisite of _private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.leadingMatrix_det_isUnit
_private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.leadingMatrix_det_isUnit._proof_1_5 is a prerequisite of _private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.leadingMatrix_det_isUnit
_private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.leadingMatrix_det_isUnit._proof_1_6 is a prerequisite of _private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.leadingMatrix_det_isUnit
_private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.parityOddEquiv._proof_1 is a prerequisite of _private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.parityOddEquiv
_private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.parityOddEquiv._proof_12 is a prerequisite of _private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.parityOddEquiv
_private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.parityOddEquiv._proof_15 is a prerequisite of _private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.parityOddEquiv
_private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.parityOddEquiv._proof_16 is a prerequisite of _private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.parityOddEquiv
_private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.parityOddEquiv._proof_2 is a prerequisite of _private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.parityOddEquiv
_private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.parityOddEquiv._proof_9 is a prerequisite of _private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.parityOddEquiv
_private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.parityOddEquiv.match_1 is a prerequisite of _private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.parityOddEquiv
_private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.blockSwap is a prerequisite of _private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.det_even_block
_private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.blockSwap_sign_int is a prerequisite of _private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.det_even_block
TheoremDB.DisjointBinarySupport.borderMatrix is a prerequisite of _private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.matrix_even_blocks
TheoremDB.DisjointBinarySupport.matrix is a prerequisite of _private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.matrix_even_blocks
_private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.land_even_even is a prerequisite of _private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.matrix_even_blocks
_private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.land_even_odd is a prerequisite of _private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.matrix_even_blocks
_private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.land_odd_even is a prerequisite of _private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.matrix_even_blocks
_private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.land_odd_odd is a prerequisite of _private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.matrix_even_blocks
_private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.parityEvenEquiv is a prerequisite of _private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.matrix_even_blocks
_private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.parityEvenEquiv_inl is a prerequisite of _private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.matrix_even_blocks
_private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.parityEvenEquiv_inr is a prerequisite of _private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.matrix_even_blocks
_private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.matrix_even_blocks._proof_1_3 is a prerequisite of _private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.matrix_even_blocks
TheoremDB.DisjointBinarySupport.matrix is a prerequisite of _private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.matrix_odd_blocks
_private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.land_even_even is a prerequisite of _private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.matrix_odd_blocks
_private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.land_odd_even is a prerequisite of _private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.matrix_odd_blocks
_private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.land_odd_odd is a prerequisite of _private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.matrix_odd_blocks
_private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.oddBorderMatrix is a prerequisite of _private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.matrix_odd_blocks
_private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.parityOddEquiv is a prerequisite of _private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.matrix_odd_blocks
_private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.matrix_odd_blocks._proof_1_4 is a prerequisite of _private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.matrix_odd_blocks
_private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.parityOddEquiv._proof_1 is a prerequisite of _private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.matrix_odd_blocks
_private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.parityOddEquiv._proof_2 is a prerequisite of _private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.matrix_odd_blocks
_private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.parityOddEquiv.match_1 is a prerequisite of _private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.matrix_odd_blocks
TheoremDB.DisjointBinarySupport.matrix is a prerequisite of TheoremDB.DisjointBinarySupport.determinant_formula_of_border_unimodular._proof_1_1
TheoremDB.DisjointBinarySupport.borderMatrix is a prerequisite of TheoremDB.DisjointBinarySupport.determinant_formula_of_border_unimodular._proof_1_2
TheoremDB.DisjointBinarySupport.matrix is a prerequisite of TheoremDB.DisjointBinarySupport.determinant_formula_of_border_unimodular._proof_1_2
TheoremDB.DisjointBinarySupport.borderMatrix is a prerequisite of TheoremDB.DisjointBinarySupport.determinant_formula_of_border_unimodular._proof_1_3
TheoremDB.DisjointBinarySupport.matrix is a prerequisite of TheoremDB.DisjointBinarySupport.determinant_formula_of_border_unimodular._proof_1_3
_private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.parityEvenEquiv is a prerequisite of _private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.parityEvenEquiv_inl
_private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.parityEvenEquiv is a prerequisite of _private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.parityEvenEquiv_inr
_private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.parityEvenEquiv_inr._proof_1_4 is a prerequisite of _private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.parityEvenEquiv_inr
_private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.parityOddEquiv._proof_3 is a prerequisite of _private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.parityOddEquiv._proof_1
_private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.parityOddEquiv._proof_4 is a prerequisite of _private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.parityOddEquiv._proof_2
_private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.blockSwap is a prerequisite of _private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.det_even_block_bottom
_private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.det_even_block is a prerequisite of _private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.det_even_block_bottom
_private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.land_even_even is a prerequisite of _private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.leadingMatrix_even_blocks
_private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.land_even_odd is a prerequisite of _private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.leadingMatrix_even_blocks
_private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.land_odd_even is a prerequisite of _private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.leadingMatrix_even_blocks
_private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.land_odd_odd is a prerequisite of _private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.leadingMatrix_even_blocks
_private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.leadingMatrix is a prerequisite of _private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.leadingMatrix_even_blocks
_private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.parityEvenEquiv is a prerequisite of _private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.leadingMatrix_even_blocks
_private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.parityEvenEquiv_inl is a prerequisite of _private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.leadingMatrix_even_blocks
_private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.parityEvenEquiv_inr is a prerequisite of _private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.leadingMatrix_even_blocks
_private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.land_even_even is a prerequisite of _private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.leadingMatrix_odd_blocks
_private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.land_even_odd is a prerequisite of _private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.leadingMatrix_odd_blocks
_private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.land_odd_even is a prerequisite of _private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.leadingMatrix_odd_blocks
_private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.land_odd_odd is a prerequisite of _private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.leadingMatrix_odd_blocks
_private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.leadingMatrix is a prerequisite of _private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.leadingMatrix_odd_blocks
_private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.leadingOddBorder is a prerequisite of _private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.leadingMatrix_odd_blocks
_private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.parityOddEquiv is a prerequisite of _private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.leadingMatrix_odd_blocks
_private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.parityOddEquiv._proof_1 is a prerequisite of _private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.leadingMatrix_odd_blocks
_private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.parityOddEquiv._proof_2 is a prerequisite of _private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.leadingMatrix_odd_blocks
_private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.parityOddEquiv.match_1 is a prerequisite of _private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.leadingMatrix_odd_blocks
_private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.finInclusion is a prerequisite of _private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.leading_odd_block_det_isUnit
_private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.leadingMatrix is a prerequisite of _private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.leading_odd_block_det_isUnit
_private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.leadingOddBorder is a prerequisite of _private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.leading_odd_block_det_isUnit
_private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.leadingOddBorder_transpose_mul_finInclusion is a prerequisite of _private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.leading_odd_block_det_isUnit
_private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.leading_mul_finInclusion is a prerequisite of _private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.leading_odd_block_det_isUnit
_private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.parityOddEquiv._proof_6 is a prerequisite of _private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.parityOddEquiv._proof_12
_private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.parityOddEquiv._proof_1 is a prerequisite of _private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.parityOddEquiv._proof_15
_private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.parityOddEquiv._proof_13 is a prerequisite of _private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.parityOddEquiv._proof_15
_private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.parityOddEquiv._proof_14 is a prerequisite of _private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.parityOddEquiv._proof_15
_private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.parityOddEquiv._proof_2 is a prerequisite of _private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.parityOddEquiv._proof_15
_private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.parityOddEquiv._proof_3 is a prerequisite of _private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.parityOddEquiv._proof_15
_private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.parityOddEquiv._proof_4 is a prerequisite of _private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.parityOddEquiv._proof_15
_private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.parityOddEquiv._proof_5 is a prerequisite of _private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.parityOddEquiv._proof_15
_private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.parityOddEquiv._proof_6 is a prerequisite of _private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.parityOddEquiv._proof_15
_private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.parityOddEquiv._proof_7 is a prerequisite of _private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.parityOddEquiv._proof_15
_private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.parityOddEquiv._proof_8 is a prerequisite of _private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.parityOddEquiv._proof_15
_private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.parityOddEquiv.match_1 is a prerequisite of _private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.parityOddEquiv._proof_15
_private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.parityOddEquiv._proof_1 is a prerequisite of _private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.parityOddEquiv._proof_16
_private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.parityOddEquiv._proof_10 is a prerequisite of _private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.parityOddEquiv._proof_16
_private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.parityOddEquiv._proof_11 is a prerequisite of _private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.parityOddEquiv._proof_16
_private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.parityOddEquiv._proof_12 is a prerequisite of _private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.parityOddEquiv._proof_16
_private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.parityOddEquiv._proof_2 is a prerequisite of _private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.parityOddEquiv._proof_16
_private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.parityOddEquiv._proof_3 is a prerequisite of _private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.parityOddEquiv._proof_16
_private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.parityOddEquiv._proof_4 is a prerequisite of _private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.parityOddEquiv._proof_16
_private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.parityOddEquiv._proof_5 is a prerequisite of _private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.parityOddEquiv._proof_16
_private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.parityOddEquiv._proof_6 is a prerequisite of _private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.parityOddEquiv._proof_16
_private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.parityOddEquiv._proof_9 is a prerequisite of _private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.parityOddEquiv._proof_16
_private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.parityOddEquiv.match_1 is a prerequisite of _private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.parityOddEquiv._proof_16
_private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.parityOddEquiv._proof_5 is a prerequisite of _private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.parityOddEquiv._proof_9
_private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.blockSwap is a prerequisite of _private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.blockSwap_sign_int
_private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.blockSwap_sign is a prerequisite of _private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.blockSwap_sign_int
_private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.finInclusion is a prerequisite of _private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.leadingOddBorder_transpose_mul_finInclusion
_private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.leadingMatrix is a prerequisite of _private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.leadingOddBorder_transpose_mul_finInclusion
_private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.leadingOddBorder is a prerequisite of _private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.leadingOddBorder_transpose_mul_finInclusion
_private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.finInclusion is a prerequisite of _private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.leading_mul_finInclusion
_private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.leadingMatrix is a prerequisite of _private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.leading_mul_finInclusion
_private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.leadingOddBorder is a prerequisite of _private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.leading_mul_finInclusion
_private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.parityOddEquiv._proof_1 is a prerequisite of _private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.parityOddEquiv._proof_13
_private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.parityOddEquiv._proof_2 is a prerequisite of _private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.parityOddEquiv._proof_13
_private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.parityOddEquiv._proof_3 is a prerequisite of _private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.parityOddEquiv._proof_13
_private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.parityOddEquiv._proof_4 is a prerequisite of _private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.parityOddEquiv._proof_13
_private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.parityOddEquiv._proof_5 is a prerequisite of _private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.parityOddEquiv._proof_13
_private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.parityOddEquiv.match_1 is a prerequisite of _private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.parityOddEquiv._proof_13
_private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.parityOddEquiv._proof_1 is a prerequisite of _private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.parityOddEquiv._proof_14
_private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.parityOddEquiv._proof_2 is a prerequisite of _private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.parityOddEquiv._proof_14
_private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.parityOddEquiv._proof_3 is a prerequisite of _private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.parityOddEquiv._proof_14
_private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.parityOddEquiv._proof_4 is a prerequisite of _private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.parityOddEquiv._proof_14
_private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.parityOddEquiv._proof_6 is a prerequisite of _private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.parityOddEquiv._proof_14
_private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.parityOddEquiv.match_1 is a prerequisite of _private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.parityOddEquiv._proof_14
_private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.blockSwap is a prerequisite of _private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.blockSwap_sign
_private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.blockSwap_fixedPoints_card is a prerequisite of _private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.blockSwap_sign
_private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.blockSwap_sq is a prerequisite of _private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.blockSwap_sign
_private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.blockSwap_sign._proof_1_1 is a prerequisite of _private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.blockSwap_sign
_private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.blockSwap is a prerequisite of _private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.blockSwap_fixedPoints_card
_private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.blockSwap is a prerequisite of _private.TheoremDB.Research.DisjointBinarySupport.0.TheoremDB.DisjointBinarySupport.blockSwap_sq

Finish Lean verification

A solution has been submitted and awaits independent review. Lean source is attached; signed verification is pending.

Continue in TheoremDB Researcher

Upload a Lean project archive

Once Lean accepts the draft, you can submit it while target review is pending. Your submission request is saved and continues after approval. Private checks stay private until you choose to submit.

1References

2 entries have incomplete source metadata. Each affected row names the fields that still need editorial review.

Packet source. Mereb, On determinants of matrices related to Pascal's triangle, Corollary 1, combined with the parity block decomposition recorded here. ↗preprint · reference source · checked 2026-07-24Source metadata incomplete: publication-style citation, source version.Source use: citation only.Source named by the research packet.Also cited at Immediate corollary of the exact determinant and unimodular-minor argument.
Bacher and Chapman, Symmetric Pascal matrices modulo p, Theorem 1.1; Mereb, arXiv:2210.12913, Corollary 1. ↗preprint · reference source · checked 2026-07-24Source metadata incomplete: publication-style citation, source version, relevance note.Source use: citation only.

Original question generated by an agent and screened by exact integer determinant computation.

Discussion

Loading discussion.

1Problem setup

2What counts as a solution

1StatusSolution submittedNot Lean-verified

1Packet records

Recent contributions

Computational notes

2See also

1Lean verification

What the formal work covers

Formal statement

Reproduce the verification

1References

Add a comment

Background

Definitions

What counts as a solution

What's known

Formal statement

Recorded work

Related work

Record & provenance

1Status