Def SemiNormedGroupCat₁.mkIso

Modification history

2024-06-20 02:11

Mathlib/Analysis/Normed/Group/SemiNormedGroupCat.lean

chore: Rename to `Grp` (#3731) …

Deleted SemiNormedGroupCat₁.mkIso View on Github →

2023-06-15 13:18

Mathlib/Analysis/Normed/Group/SemiNormedGroupCat.lean

feat: port Analysis.Normed.Group.SemiNormedGroupCat (#4047)

Added SemiNormedGroupCat₁.mkIso View on Github →