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: Jul 25 2024 at 16:02 UTC