Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-04-19 23:26 71b470f9

View on Github →

chore(analysis/normed_space/star): make an argument explicit (#13523)

Estimated changes

Modified src/analysis/normed_space/star/basic.lean

modified theorem nnnorm_star

Modified src/analysis/normed_space/star/matrix.lean

Modified src/topology/continuous_function/bounded.lean

Modified src/topology/continuous_function/zero_at_infty.lean