IsModuleFiltration

Stream: mathlib4

[Jovan Gerbscheid]

While working on lean#9638, I found out that IsModuleFiltration is a bad use of extends:

class IsModuleFiltration (F : ι → σ) (F_lt : outParam <| ι → σ) [IsRingFiltration F F_lt]
    (F' : ιM → σM) (F'_lt : outParam <| ιM → σM) : Prop
    extends IsFiltration F' F'_lt, SetLike.GradedSMul F F'

This is bad because the instance IsModuleFiltration.toIsFiltration in principle cannot determine the value of F. Should IsFiltration be a (normal) field of the structure, or a parameter similar to [IsRingFiltration F F_lt]? (@Nailin Guan)

[Nailin Guan]

I didn't notice it before, if this did help synthizing work, I have nothing against this. I will have a look asap.