Structures · Algebra
GroupSeminormClass
GroupSeminormClass F α states that F is a type of β-valued seminorms on the group α.
You should extend this class when you extend GroupSeminorm.
- Defined in
- Mathlib.Algebra.Order.Hom.Basic
- Shape
- 3 explicit arguments · adds map_one_eq_zero, map_inv_eq_map
Extends1
Extended by1
Concrete types that are instances1
- GroupSeminorm
How is a type an instance?
Loading the hierarchy index…
Assumed by13
- GroupSeminormClass.map_inv_eq_map
- GroupSeminormClass.map_one_eq_zero
- GroupSeminormClass.toSeminormedCommGroup
- map_div_rev
- le_map_add_map_div'
- GroupSeminormClass.toSeminormedGroup
- GroupSeminormClass.toNonnegHomClass
- map_div_le_add
- GroupSeminormClass.toSeminormedCommGroup_norm_eq
- GroupSeminormClass.toSeminormedGroup_norm_eq
- abs_sub_map_le_div
- GroupSeminormClass.toMulLEAddHomClass
- map_inv_mul