Theorem NormedAddGroupHom.isQuotientQuotient

Modification history

2023-05-08 00:54

Mathlib/Analysis/Normed/Group/Quotient.lean

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

Added NormedAddGroupHom.isQuotientQuotient View on Github →