Theorem SeparationQuotient.norm_liftNormedAddGroupHom_apply_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.norm_liftNormedAddGroupHom_apply_le View on Github →