Theorem SeparationQuotient.liftNormedAddGroupHom_normNoninc

Modification history

2025-02-05 23:29
Mathlib/Analysis/Normed/Group/SeparationQuotient.lean
feat(Analysis/Normed/Group/SeparationQuotient): add normed lifts and `mk` (#18178) …
Added SeparationQuotient.liftNormedAddGroupHom_normNonincView on Github →