equal
deleted
inserted
replaced
3 *) |
3 *) |
4 |
4 |
5 header {* Inner Product Spaces and the Gradient Derivative *} |
5 header {* Inner Product Spaces and the Gradient Derivative *} |
6 |
6 |
7 theory Inner_Product |
7 theory Inner_Product |
8 imports Complex FrechetDeriv |
8 imports Complex_Main FrechetDeriv |
9 begin |
9 begin |
10 |
10 |
11 subsection {* Real inner product spaces *} |
11 subsection {* Real inner product spaces *} |
12 |
12 |
13 class real_inner = real_vector + sgn_div_norm + |
13 class real_inner = real_vector + sgn_div_norm + |