Zulip Chat Archive

Stream: condensed mathematics

Topic: PFPNGWT?

Mario Carneiro (Mar 25 2021 at 17:06):

Is there a category corresponding to profinitely_filtered_pseudo_normed_group_with_Tinv_hom?

Johan Commelin (Mar 25 2021 at 17:17):

@Mario Carneiro Yes, that is ProFiltPseuNormGrpWithTinv

Johan Commelin (Mar 25 2021 at 17:18):

https://github.com/leanprover-community/lean-liquid/blob/master/src/pseudo_normed_group/category.lean#L16

Last updated: May 02 2025 at 03:31 UTC