Stream: math-comp users

Topic: ✔ Proving linearity is closed on function add/scale


view this post on Zulip abab9579 (Aug 24 2022 at 09:08):

I am trying to prove that linearity is closed on function addition/scaling.
Before proceeding with proof, I want to check if this fact is already proved, or there is helpful lemmas to prove this one.
That is, is there something to help me prove linear f -> linear g -> linear (f \+ g) and linear f -> linear (a \o* f)?

view this post on Zulip Pierre Roux (Aug 24 2022 at 09:31):

For the first one, one can find add_fun_is_additive and add_fun_is_scalable in file ssralg.v, along with canonical declarations (just below the lemmas in the file) ensuring that if f and g are canonically linear then f \+ g is also canonically linear (meaning it can be used with any lemma requiring a {linear _ -> _}). Same thing for f \o* g.

view this post on Zulip abab9579 (Aug 24 2022 at 11:12):

I see, strange that I cannot find add_fun_is_additive even though I imported ssralg.

view this post on Zulip Pierre Roux (Aug 24 2022 at 11:46):

Indeed, it is inside a module (GRing) and is not exported since it is only used to build canonical instances (which are exported).

view this post on Zulip abab9579 (Aug 24 2022 at 11:54):

Can I access such non-exported definitions, or is it impossible? I could work around it, but direct access will be more convenient.

view this post on Zulip Paolo Giarrusso (Aug 24 2022 at 12:20):

you just need to import the containing modules explicitly

view this post on Zulip abab9579 (Aug 25 2022 at 01:00):

Oh, that is simpler than I expected. Anyway, it turnedd out that the lemmas are not so useful for me. Still, I appreciate your help a lot!

view this post on Zulip Notification Bot (Aug 25 2022 at 01:00):

abab9579 has marked this topic as resolved.


Last updated: Oct 13 2024 at 01:02 UTC