Theorem SeparationQuotient.liftNormedAddGroupHom_norm_le

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_norm_le View on Github →