Commit 2021-01-29 17:21 0d18179a
View on Github →chore(analysis/normed_space/multilinear): rename variables (#5929)
Use E
and E'
for indexed types and G
and G'
for Type*
s.
chore(analysis/normed_space/multilinear): rename variables (#5929)
Use E
and E'
for indexed types and G
and G'
for Type*
s.