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