Structures · Algebra

AddGroupSeminormClass

AddGroupSeminormClass F α states that F is a type of β-valued seminorms on the additive group α. You should extend this class when you extend AddGroupSeminorm.

Defined in

Mathlib.Algebra.Order.Hom.Basic

Shape

3 explicit arguments · adds map_zero, map_neg_eq_map