Theorem AddSubgroup.normedMk.apply

Modification history

2023-05-08 00:54

Mathlib/Analysis/Normed/Group/Quotient.lean

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

Added AddSubgroup.normedMk.apply View on Github →