The determinant inequality, assembled

The determinant inequality (Corollary 3.2 of the paper), from the two halves of its proof:

• AaronsonAmbainis.DetLow.lowestUnit, AaronsonAmbainis.DetLow.lowestBound (directory DetLow),
• AaronsonAmbainis.DetBij.detInequality_of_lowest (directory DetBij).

theorem AaronsonAmbainis.detInequality : DetInequality

The determinant inequality (Corollary 3.2 of the paper), with no hypothesis.