Structures · Algebra
IsRingFiltration
For a family of subsets σ of semiring R, an increasing series F in σ is
a ring filtration if IsFiltration F F_lt and the pointwise multiplication of F i and F j
is in F (i + j).
- Defined in
- Mathlib.RingTheory.FilteredAlgebra.Basic
- Shape
- 2 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…