Structures · Algebra
RingSeminormClass
RingSeminormClass F α states that F is a type of β-valued seminorms on the ring α.
You should extend this class when you extend RingSeminorm.
- Defined in
- Mathlib.Algebra.Order.Hom.Basic
- Shape
- 3 explicit arguments
Extends2
Extended by1
Concrete types that are instances1
- RingSeminorm
How is a type an instance?
Loading the hierarchy index…