Diffusion Isabelle 409ca22dee4c

new notion of infinite sums in HOL-Analysis, ordering on complex numbers
409ca22dee4c
Actions

Tags

None

Subscribers

None

Description

new notion of infinite sums in HOL-Analysis, ordering on complex numbers

Details

Provenance

Authored on

Parents

rISABELLE253c98aa935a: NEWS and CONTRIBUTORS

Branches

Unknown

Tags

Unknown

Event Timeline

pruvisto committed rISABELLE409ca22dee4c: new notion of infinite sums in HOL-Analysis, ordering on complex numbers.Oct 6 2021, 2:19 PM

pruvisto mentioned this in rAFPd6153e63e6cb: adapted to isabelle-dev/409ca22dee4c.Oct 7 2021, 12:59 PM

pruvisto mentioned this in rAFPf8ba1eaa5cec: adapted QHLProver to isabelle-dev/409ca22dee4c.Oct 7 2021, 10:21 PM

Changes (18)

Path

Size

Infinite_Set_Sum.thy

Infinite_Sum.thy

Product_Vector.thy

document/

Complex_Analysis/

Winding_Numbers.thy

Complex_Order.thy

Extended_Nonnegative_Real.thy

Real_Vector_Spaces.thy

Topological_Spaces.thy

rISABELLE409ca22dee4c

CONTRIBUTORS

Loading...

NEWS

Loading...

src/HOL/Analysis/Analysis.thy

Loading...

src/HOL/Analysis/Infinite_Set_Sum.thy

Loading...

src/HOL/Analysis/Infinite_Sum.thy

Loading...

src/HOL/Analysis/Product_Vector.thy

Loading...

src/HOL/Analysis/document/root.bib

Loading...

src/HOL/Complex_Analysis/Winding_Numbers.thy

Loading...

src/HOL/Library/Complex_Order.thy

Loading...

src/HOL/Library/Extended_Nonnegative_Real.thy

Loading...

src/HOL/Limits.thy

Loading...

src/HOL/ROOT

Loading...

src/HOL/Real_Vector_Spaces.thy

Loading...

src/HOL/Topological_Spaces.thy

Loading...