Structure NormedAddGroupHom.IsQuotient

Modification history

2023-05-08 00:54

Mathlib/Analysis/Normed/Group/Quotient.lean

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

Added NormedAddGroupHom.IsQuotient View on Github →