where to put the kernels lemma

Stream: mathlib4

[Thomas Moulin]

Hey everyone, I implemented the kernels lemma from the missing undergraduate mathematics in mathib, and I was wondering where to put the main results as well as some intermediate results needed for the main result ?

I have stuff about endormphisms but also polynomials so I am hesitating between
Mathlib/Algebra/Polynomial
Mathlib/RingTheory/Polynomial/
Mathlib/Algebra/Module/LinearMap

This will be my first contribution, I am new and still having some difficulty understanding what to put where.

The results have the following signatures:
-(f : Module.End K E) (s : Finset ι) (P : ι → K[X]) (i : ι) (hi : i ∈ s): (P i |>.smeval f).ker ≤ (s.prod P |>.smeval f).ker

-(f : Module.End K E) (s : Finset ι) (P : ι → K[X]) (hs : s.Nonempty) (h : (s : Set ι).Pairwise <| IsCoprime.onFun P): (s.prod P |>.smeval f).ker ≤ ⨆ i ∈ s, (P i |>.smeval f).ker

-(f : Module.End K E) (s : Finset ι) (P : ι → K[X]) (h : (s : Set ι).Pairwise <| IsCoprime.onFun P): (s.prod P |>.smeval f).ker = ⨆ i ∈ s, (P i |>.smeval f).ker

For now i have them under the LinearMap namespace, on a separate file Mathlib/RingTheory/Polynomial/KernelDecomposition.lean but i don't fell like having an authored file for my first contribution.

Thanks!

[Weiyi Wang]

You probably want to put your code inside ``` for better formatting