PanSkanderaWangAllSplitsReverse

Abstract

The defining submatrix expression reverses both rows and columns.

Definition 1.1 (reverseMatrix).

$$\forall n\in \mathbb{N},\forall A\in \mathrm{Matrix}\left(\mathrm{Fin}\left(n\right),\mathrm{Fin}\left(n\right),\mathbb{R}\right),\mathrm{reverseMatrix}\left(A\right)=\mathrm{submatrix}\left(A,\mathrm{FinRev}\left(n\right),\mathrm{FinRev}\left(n\right)\right)$$

Formalization. D5/S3/Combinatorics/Permanental/PanSkanderaWangAllSplitsReverse.reverseMatrix (✓ std3).

Source. Repository-derived.

Acknowledgement. Sihong Pan, Mark Skandera, Jiayuan Wang (2026). Permanental Inequalities and Unit Interval Orders. DOI: 10.4204/EPTCS.445.17. URL: https://arxiv.org/abs/2606.13162v1.

Commentary.

The defining submatrix expression reverses both rows and columns. FinRev(n) is the function Fin.rev on Fin n.

References

• Truth anchor: D5/S3/Combinatorics/Permanental/PanSkanderaWangAllSplitsReverse.reverseMatrix
• Dependency: D5/S3/Combinatorics/Permanental/PanSkanderaWangAllSplitsPermanentPadding