Diffusion afp-devel 22721115789f

Miscellaneous changes to Complex_Bounded_Operators.
22721115789f
Actions

Tags

None

Subscribers

None

Description

Miscellaneous changes to Complex_Bounded_Operators.

Details

Provenance

Dominique Unruh <hg.yse9he@rwth.unruh.de>

Authored on

Parents

rAFPe3e5ef410780: Frequency_Moments: Add tutorial on pseudorandom objects.

Branches

Unknown

Tags

Unknown

Event Timeline

Dominique Unruh <hg.yse9he@rwth.unruh.de> committed rAFP22721115789f: Miscellaneous changes to Complex_Bounded_Operators..Sat, Apr 20, 11:29 PM

Changes (8)

Path

Size

thys/

Complex_Bounded_Operators/

Complex_Bounded_Linear_Function.thy

Complex_Inner_Product.thy

Complex_Inner_Product0.thy

Complex_Vector_Spaces.thy

One_Dimensional_Spaces.thy

extra/

Extra_Ordered_Fields.thy

Extra_Vector_Spaces.thy

rAFP22721115789f

thys/Complex_Bounded_Operators/Complex_Bounded_Linear_Function.thy

Loading...

thys/Complex_Bounded_Operators/Complex_Inner_Product.thy

Loading...

thys/Complex_Bounded_Operators/Complex_Inner_Product0.thy

Loading...

thys/Complex_Bounded_Operators/Complex_L2.thy

Loading...

thys/Complex_Bounded_Operators/Complex_Vector_Spaces.thy

Loading...

thys/Complex_Bounded_Operators/One_Dimensional_Spaces.thy

Loading...

thys/Complex_Bounded_Operators/extra/Extra_Ordered_Fields.thy

Loading...

thys/Complex_Bounded_Operators/extra/Extra_Vector_Spaces.thy

Loading...