Commit 2025-02-05 23:58 f6895b22

View on Github →

refactor(Analysis/Normed): ConcreteCategory refactor for SemiNormedGrp (#21477) This PR adds a Hom structure and ConcreteCategory instance for SemiNormedGrp and SemiNormedGrp_1. Zulip thread: https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Concrete.20category.20class.20redesign

Estimated changes

added structure SemiNormedGrp.Hom
added theorem SemiNormedGrp.hom_add
added theorem SemiNormedGrp.hom_comp
added theorem SemiNormedGrp.hom_ext
added theorem SemiNormedGrp.hom_id
added theorem SemiNormedGrp.hom_neg
added theorem SemiNormedGrp.hom_nsum
added theorem SemiNormedGrp.hom_sub
added theorem SemiNormedGrp.hom_zero
added theorem SemiNormedGrp.hom_zsum
added theorem SemiNormedGrp.id_apply
deleted def SemiNormedGrp.of
added theorem SemiNormedGrp.ofHom_id
added structure SemiNormedGrp
deleted def SemiNormedGrp
added structure SemiNormedGrp₁.Hom
added theorem SemiNormedGrp₁.ext
modified theorem SemiNormedGrp₁.hom_ext
deleted def SemiNormedGrp₁.of
added structure SemiNormedGrp₁
deleted def SemiNormedGrp₁