Commit 2023-07-10 06:57 71a32bff

View on Github →

feat: port Analysis.Normed.Group.SemiNormedGroup.Completion (#5697)

Estimated changes

Modified Mathlib.lean

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

added def SemiNormedGroupCat.completion.incl

added def SemiNormedGroupCat.completion.lift

added theorem SemiNormedGroupCat.completion.lift_comp_incl

added theorem SemiNormedGroupCat.completion.lift_unique

added def SemiNormedGroupCat.completion.mapHom

added theorem SemiNormedGroupCat.completion.map_normNoninc

added theorem SemiNormedGroupCat.completion.map_zero

added theorem SemiNormedGroupCat.completion.norm_incl_eq

added def SemiNormedGroupCat.completion