Diffusion afp-devel d6153e63e6cb

adapted to isabelle-dev/409ca22dee4c
d6153e63e6cb
Actions

Tags

None

Subscribers

None

Description

adapted to isabelle-dev/409ca22dee4c

Details

Provenance

Authored on

Parents

rAFPc0285f96e2f4: adapted to devel

Branches

Unknown

Tags

Unknown

Event Timeline

pruvisto committed rAFPd6153e63e6cb: adapted to isabelle-dev/409ca22dee4c.Oct 7 2021, 12:58 PM

Changes (15)

Path

Size

thys/

Complex_Bounded_Operators/

Complex_Bounded_Linear_Function.thy

Complex_Euclidean_Space0.thy

Complex_Inner_Product.thy

Complex_Inner_Product0.thy

extra/

Extra_General.thy

Extra_Jordan_Normal_Form.thy

Extra_Ordered_Fields.thy

Count_Complex_Roots/

Count_Complex_Roots.thy

Jordan_Normal_Form/

LLL_Basis_Reduction/

Prime_Distribution_Elementary/

Partial_Zeta_Bounds.thy

Projective_Measurements/

Linear_Algebra_Complements.thy

Projective_Measurements.thy

QHLProver/

Complex_Matrix.thy

Stirling_Formula/

Gamma_Asymptotics.thy

rAFPd6153e63e6cb

thys/Complex_Bounded_Operators/Complex_Bounded_Linear_Function.thy

Loading...

thys/Complex_Bounded_Operators/Complex_Euclidean_Space0.thy

Loading...

thys/Complex_Bounded_Operators/Complex_Inner_Product.thy

Loading...

thys/Complex_Bounded_Operators/Complex_Inner_Product0.thy

Loading...

thys/Complex_Bounded_Operators/extra/Extra_General.thy

Loading...

thys/Complex_Bounded_Operators/extra/Extra_Jordan_Normal_Form.thy

Loading...

thys/Complex_Bounded_Operators/extra/Extra_Ordered_Fields.thy

Loading...

thys/Count_Complex_Roots/Count_Complex_Roots.thy

Loading...

thys/Jordan_Normal_Form/Conjugate.thy

Loading...

thys/LLL_Basis_Reduction/Norms.thy

Loading...

thys/Prime_Distribution_Elementary/Partial_Zeta_Bounds.thy

Loading...

thys/Projective_Measurements/Linear_Algebra_Complements.thy

Loading...

thys/Projective_Measurements/Projective_Measurements.thy

Loading...

thys/QHLProver/Complex_Matrix.thy

Loading...

thys/Stirling_Formula/Gamma_Asymptotics.thy

Loading...