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)
?
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
.
I see, strange that I cannot find add_fun_is_additive
even though I imported ssralg
.
Indeed, it is inside a module (GRing) and is not exported since it is only used to build canonical instances (which are exported).
Can I access such non-exported definitions, or is it impossible? I could work around it, but direct access will be more convenient.
you just need to import the containing modules explicitly
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!
abab9579 has marked this topic as resolved.
Last updated: Oct 13 2024 at 01:02 UTC