Diffusion afp-devel 79e09cd07d73

removed precondition in det_four_block_mat
79e09cd07d73
Actions

Tags

None

Subscribers

None

Description

removed precondition in det_four_block_mat

Details

Provenance

Rene Thiemann <rene.thiemann@uibk.ac.at>

Authored on

Parents

rAFPf0ff48f384e9: merge

Branches

Unknown

Tags

Unknown

Event Timeline

Rene Thiemann <rene.thiemann@uibk.ac.at> committed rAFP79e09cd07d73: removed precondition in det_four_block_mat.Jul 4 2022, 5:37 PM

Changes (2)

Path

Size

thys/

Jordan_Normal_Form/

Determinant.thy

Linear_Inequalities/

Integral_Bounded_Vectors.thy

rAFP79e09cd07d73

thys/Jordan_Normal_Form/Determinant.thy

Loading...

thys/Linear_Inequalities/Integral_Bounded_Vectors.thy

Loading...