Commit 2023-07-06 13:41 28d08e7f

View on Github →

feat: port Analysis.Normed.Group.SemiNormedGroup.Kernels (#5085)

Estimated changes

Modified Mathlib.lean

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

added theorem SemiNormedGroupCat.ExplicitCoker.map_desc

added def SemiNormedGroupCat.cokernelCocone

added def SemiNormedGroupCat.cokernelLift

added theorem SemiNormedGroupCat.comp_explicitCokernelπ

added def SemiNormedGroupCat.explicitCokernel

added def SemiNormedGroupCat.explicitCokernelDesc

added theorem SemiNormedGroupCat.explicitCokernelDesc_comp_eq_desc

added theorem SemiNormedGroupCat.explicitCokernelDesc_comp_eq_zero

added theorem SemiNormedGroupCat.explicitCokernelDesc_normNoninc

added theorem SemiNormedGroupCat.explicitCokernelDesc_norm_le

added theorem SemiNormedGroupCat.explicitCokernelDesc_norm_le_of_norm_le

added theorem SemiNormedGroupCat.explicitCokernelDesc_unique

added theorem SemiNormedGroupCat.explicitCokernelDesc_zero

added def SemiNormedGroupCat.explicitCokernelIso

added theorem SemiNormedGroupCat.explicitCokernelIso_hom_desc

added theorem SemiNormedGroupCat.explicitCokernelIso_hom_π

added theorem SemiNormedGroupCat.explicitCokernelIso_inv_π

added theorem SemiNormedGroupCat.explicitCokernel_hom_ext

added def SemiNormedGroupCat.explicitCokernelπ

added theorem SemiNormedGroupCat.explicitCokernelπ_apply_dom_eq_zero

added theorem SemiNormedGroupCat.explicitCokernelπ_desc

added theorem SemiNormedGroupCat.explicitCokernelπ_desc_apply

added theorem SemiNormedGroupCat.explicitCokernelπ_surjective

added def SemiNormedGroupCat.fork

added def SemiNormedGroupCat.isColimitCokernelCocone

added theorem SemiNormedGroupCat.isQuotient_explicitCokernelπ

added theorem SemiNormedGroupCat.normNoninc_explicitCokernelπ

added def SemiNormedGroupCat₁.cokernelCocone

added def SemiNormedGroupCat₁.cokernelLift