Fitting's Lemma

Stream: new members

[VayusElytra]

I was looking through the documentation concerning Fitting's Lemma (here); how can one use this to actually obtain a decomposition of some module M as a product of image and kernel of a power of an endomorphism? In particular the implementation makes no reference to products at all. Is this a bit of API that it would be useful to prove and contribute to mathlib?

[Sophie Morel]

The decomposition is hidden in the properties of IsCompl for submodule, more precisely there

[VayusElytra]

Thank you! Just one more question; what's the ∀ᶠ n in atTop in the statement of eventually_codisjoint_ker_pow_range_pow in Mathlib.RingTheory.Artinian? The old implementation of this theorem just used exists n; why is the new version preferable?

[Filippo A. E. Nuccio]

This is described in docs#Filter.Eventually. It is the notation meaning "for every sufficiently large n (without specifying who n actually is).

[Filippo A. E. Nuccio]

The new implementation is finer: it says that once you have found one n that works, all larger m will also work.