Theorems · Inductive type · functional analysis

GroupNorm

(G : Type u_6) → [Group G] → Type u_6

A seminorm on a group G is a function f : G → ℝ that sends one to zero, is submultiplicative and such that f x⁻¹ = f x and f x = 0 → x = 1 for all x.

Defined in

Mathlib.Analysis.Normed.Group.Seminorm

Cited by

15 results in Mathlib

Foundations

Depth 1 from the axioms · uses no axioms

Assumes

Group