Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-02-02 18:29 2b2edc97

View on Github →

chore(analysis/normed_space/basic): use explicit arg 𝕜' in lemmas about normed_algebra (#6009)

Estimated changes