Commit 2023-05-29 17:56 837f72de
View on Github →chore(analysis/normed/group/add_torsor): nnnorm lemmas (#18997)
For every dist
/norm
lemma in these files, this adds the corresponding nndist
/nnnorm
lemma.
chore(analysis/normed/group/add_torsor): nnnorm lemmas (#18997)
For every dist
/norm
lemma in these files, this adds the corresponding nndist
/nnnorm
lemma.