Diffusion afp-devel c51cd33d81da

Complex_Bounded_Operators: Added numerous new lemmas.
c51cd33d81da
Actions

Tags

None

Subscribers

None

Description

Complex_Bounded_Operators: Added numerous new lemmas.

Details

Provenance

Dominique Unruh <unruh@ut.ee>

Authored on

Parents

rAFP2d501ecd4932: Merged

Branches

Unknown

Tags

Unknown

Event Timeline

Dominique Unruh <unruh@ut.ee> committed rAFPc51cd33d81da: Complex_Bounded_Operators: Added numerous new lemmas..Sep 20 2022, 1:00 PM

Changes (5)

Path

Size

thys/

Complex_Bounded_Operators/

Complex_Bounded_Linear_Function.thy

Complex_Inner_Product.thy

Complex_Vector_Spaces.thy

extra/

Extra_General.thy

rAFPc51cd33d81da

thys/Complex_Bounded_Operators/Complex_Bounded_Linear_Function.thy

Loading...

thys/Complex_Bounded_Operators/Complex_Inner_Product.thy

Loading...

thys/Complex_Bounded_Operators/Complex_L2.thy

Loading...

thys/Complex_Bounded_Operators/Complex_Vector_Spaces.thy

Loading...

thys/Complex_Bounded_Operators/extra/Extra_General.thy

Loading...