Stream: Hierarchy Builder devs & users

Topic: ✔ How should I go with ssralg's linear-like structure?

view this post on Zulip abab9579 (Sep 11 2022 at 14:05):

Sorry, I think I was not being clear. What I want is making a type CInfty with notation {cinfty U -> V}, and ability to

  1. Create a substructure of CInfty later
  2. MkCInfty notation to construct {cinfty U -> V} from the proof that given function is C-infinity.
  3. Ability to do [cinfty of (f \+ g)] for f, g with cinfty structure. (C-infinity is also closed in addition)
    In addition, I want to attach e.g. zmodType on {cinfty U -> V}.

CInfty would not be substructure of Linear, so I do not need to care about internals of linear.

view this post on Zulip Pierre Roux (Sep 11 2022 at 14:11):

Sure, but you can take inspiration of how linear is done to craft your CInfty.

view this post on Zulip abab9579 (Sep 11 2022 at 14:13):

I see what you mean now. Thank you!

view this post on Zulip Notification Bot (Sep 11 2022 at 14:13):

abab9579 has marked this topic as resolved.

Last updated: Jan 29 2023 at 16:02 UTC