Theorem quotient_norm_nonneg

Modification history

2023-05-08 00:54

Mathlib/Analysis/Normed/Group/Quotient.lean

feat: port Analysis.Normed.Group.Quotient (#3457)

Added quotient_norm_nonneg View on Github →