Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-02-18 17:07 0c2dbd56

View on Github →

chore(analysis/normed_space/basic): implicit args (#2011) Arguments to these iffs should be implicit.

Estimated changes

Modified src/analysis/asymptotics.lean

Modified src/analysis/calculus/deriv.lean

Modified src/analysis/calculus/fderiv.lean

Modified src/analysis/calculus/tangent_cone.lean

Modified src/analysis/normed_space/banach.lean

Modified src/analysis/normed_space/basic.lean

modified theorem nnnorm_eq_zero

modified theorem norm_eq_zero

modified theorem norm_le_zero_iff

modified theorem norm_pos_iff

modified theorem norm_zero

Modified src/analysis/normed_space/multilinear.lean

Modified src/analysis/normed_space/operator_norm.lean

Modified src/analysis/specific_limits.lean

Modified src/data/padics/hensel.lean

Modified src/data/padics/padic_numbers.lean

Modified src/measure_theory/simple_func_dense.lean

Modified src/topology/metric_space/cau_seq_filter.lean