Stream: Is there code for X?
Topic: add_subgroup of normed_group
Johan Commelin (Dec 31 2020 at 10:22):
Does mathlib know that additive subgroups of normed groups are normed groups?
Yury G. Kudryashov (Dec 31 2020 at 20:19):
According to docs#normed_group, no
Johan Commelin (Dec 31 2020 at 20:22):
thanks... I'll PR something in the next few days, I guess.
Last updated: May 17 2021 at 16:26 UTC