Commit 2023-06-15 13:18 0fc56964

View on Github →

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

Estimated changes

Modified Mathlib.lean

Created Mathlib/Analysis/Normed/Group/SemiNormedGroupCat.lean

added theorem SemiNormedGroupCat.coe_comp

added theorem SemiNormedGroupCat.coe_id

added theorem SemiNormedGroupCat.coe_of

added theorem SemiNormedGroupCat.ext

added theorem SemiNormedGroupCat.isZero_of_subsingleton

added theorem SemiNormedGroupCat.iso_isometry_of_normNoninc

added def SemiNormedGroupCat.of

added theorem SemiNormedGroupCat.zero_apply

added def SemiNormedGroupCat

added theorem SemiNormedGroupCat₁.coe_comp

added theorem SemiNormedGroupCat₁.coe_id

added theorem SemiNormedGroupCat₁.coe_of

added theorem SemiNormedGroupCat₁.hom_ext

added theorem SemiNormedGroupCat₁.isZero_of_subsingleton

added theorem SemiNormedGroupCat₁.iso_isometry

added def SemiNormedGroupCat₁.mkHom

added theorem SemiNormedGroupCat₁.mkHom_apply

added def SemiNormedGroupCat₁.mkIso

added def SemiNormedGroupCat₁.of

added theorem SemiNormedGroupCat₁.zero_apply

added def SemiNormedGroupCat₁