Mathlib v3 is deprecated. Go to Mathlib v4

Theorem SemiNormedGroup.explicit_cokernel_desc_norm_le_of_norm_le

Modification history

2021-07-30 07:20

src/analysis/normed_space/SemiNormedGroup/kernels.lean

feat(analysis/normed_space/SemiNormedGroup/kernel): Fix universes + add explicit (#8467) …

Added SemiNormedGroup.explicit_cokernel_desc_norm_le_of_norm_le View on Github →