HomeIsabelle/Phabricator
Diffusion afp-devel b3ed7312e4c8

Complex_Bounded_Operators: Replaced use of HOL-Analysis.Infinite_Set_Sum by HOL…
b3ed7312e4c8
Actions

Description

Complex_Bounded_Operators: Replaced use of HOL-Analysis.Infinite_Set_Sum by HOL-Analysis.Infinite_Sum

Details

Provenance
Dominique Unruh <unruh@ut.ee>Authored on
Parents
rAFP4c2a8ccf67f4: Banach_Steinhaus: Removed unused theory dependency Infinite_Set_Sum
Branches
Unknown
Tags
Unknown

Changes (14)

PathSize

rAFPb3ed7312e4c8

View Options

thys/Complex_Bounded_Operators/Cblinfun_Code.thy

Loading...
View Options

thys/Complex_Bounded_Operators/Cblinfun_Matrix.thy

Loading...
View Options

thys/Complex_Bounded_Operators/Complex_Bounded_Linear_Function.thy

Loading...
View Options

thys/Complex_Bounded_Operators/Complex_Euclidean_Space0.thy

Loading...
View Options

thys/Complex_Bounded_Operators/Complex_Inner_Product.thy

Loading...
View Options

thys/Complex_Bounded_Operators/Complex_Inner_Product0.thy

Loading...
View Options

thys/Complex_Bounded_Operators/Complex_L2.thy

Loading...
View Options

thys/Complex_Bounded_Operators/Complex_Vector_Spaces0.thy

Loading...
View Options

thys/Complex_Bounded_Operators/extra/Extra_General.thy

Loading...
View Options

thys/Complex_Bounded_Operators/extra/Extra_Infinite_Set_Sum.thy

Loading...
View Options

thys/Complex_Bounded_Operators/extra/Extra_Ordered_Fields.thy

Loading...