Mathlib v3 is deprecated. Go to Mathlib v4

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.

Estimated changes