Structures · Algebra
IsModuleFiltration
For F satisfying IsRingFiltration F F_lt in a semiring R and σM a family of subsets of
an R-module M, an increasing series FM in σM is a module filtration if IsFiltration F F_lt
and the pointwise scalar multiplication of F i and FM j is in F (i +ᵥ j).
The index set ιM for the module can be more general, however usually we take ιM = ι.
- Defined in
- Mathlib.RingTheory.FilteredAlgebra.Basic
- Shape
- 4 explicit arguments
Extends2
Extended by0
Nothing extends this class yet.
Concrete types that are instances0
No instance on a concrete type; it is reached through other classes.
How is a type an instance?
Loading the hierarchy index…