HomeIsabelle/Phabricator

renamed det_bound_gram to det_bound_hadamard, showed that bound is tight (using…

Description

renamed det_bound_gram to det_bound_hadamard, showed that bound is tight (using unproven fact about determinants of block-matrices)