Type specialization

Stream: new members

[Magalame]

Hi, is there a way to specialize types ? What I mean is I have two complex inner product spaces A, B and I'd want a type C := A →L[ℂ] B for the sake of readability. I have tried

structure lin_bounded_map (A: Type) [inner_product_space  ℂ A] (B:Type) [inner_product_space ℂ B] extends  A →L[ℂ] B

but when asking for a A →L[ℂ] B the compiler isnt happy with me providing a lin_bounded_map A B instead. I imagine I can do

structure lin_bounded_map (A: Type) [inner_product_space  ℂ A] (B:Type) [inner_product_space ℂ B] : Type :=
(to_func: A →L[ℂ] B)

but it seems suboptimal

[Andrew Yang]

What you want is probably

def lin_bounded_map (A: Type) [inner_product_space  ℂ A] (B:Type) [inner_product_space ℂ B] : Type :=
A →L[ℂ] B

[Eric Wieser]

Right; Andrew Yang's answer is "don't extend things if you're not actually adding any new fields".

If you were adding new fields, then the answer is sometimes docs#continuous_linear_map_class, which lets you register that lin_bounded_map "is" a continuous linear map

[Magalame]

excellent thanks a lot!