Theorems · Inductive type · order theory

GroupNormClass

(F : Type u_7) →
  (α : outParam (Type u_8)) →
    (β : outParam (Type u_9)) → [Group α] → [AddCommMonoid β] → [PartialOrder β] → [FunLike F α β] → Prop

GroupNormClass F α states that F is a type of β-valued norms on the group α. You should extend this class when you extend GroupNorm.

Defined in

Mathlib.Algebra.Order.Hom.Basic

Cited by

6 results in Mathlib

Foundations

Depth 3 from the axioms · uses no axioms

Assumes

GroupAddCommMonoidPartialOrderFunLike