Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-07-30 07:20 98b0d18a

View on Github →

feat(analysis/normed_space/SemiNormedGroup/kernel): Fix universes + add explicit (#8467) See associated discussion from zulip

Estimated changes

Modified src/analysis/normed_space/SemiNormedGroup/kernels.lean

added def SemiNormedGroup.cokernel_cocone

added def SemiNormedGroup.cokernel_lift

added theorem SemiNormedGroup.comp_explicit_cokernel_π

added def SemiNormedGroup.explicit_cokernel

added def SemiNormedGroup.explicit_cokernel_desc

added theorem SemiNormedGroup.explicit_cokernel_desc_norm_le

added theorem SemiNormedGroup.explicit_cokernel_desc_norm_le_of_norm_le

added theorem SemiNormedGroup.explicit_cokernel_desc_unique

added theorem SemiNormedGroup.explicit_cokernel_hom_ext

added def SemiNormedGroup.explicit_cokernel_iso

added theorem SemiNormedGroup.explicit_cokernel_iso_hom_desc

added theorem SemiNormedGroup.explicit_cokernel_iso_hom_π

added theorem SemiNormedGroup.explicit_cokernel_iso_inv_π

added def SemiNormedGroup.explicit_cokernel_π

added theorem SemiNormedGroup.explicit_cokernel_π_desc

added def SemiNormedGroup.is_colimit_cokernel_cocone

added theorem SemiNormedGroup.is_quotient_explicit_cokernel_π

added theorem SemiNormedGroup.norm_noninc_explicit_cokernel_π

modified def SemiNormedGroup₁.cokernel_cocone

modified def SemiNormedGroup₁.cokernel_lift