Theorem quotient_norm_add_le

Modification history

2025-07-07 17:19

Mathlib/Analysis/Normed/Group/Quotient.lean

chore: golf using `exact` (#26654)

Modified quotient_norm_add_le View on Github →

2023-05-08 00:54

Mathlib/Analysis/Normed/Group/Quotient.lean

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

Added quotient_norm_add_le View on Github →