Commit 2019-03-26 19:07 df08058b

View on Github →

refactor(analysis/normed_space): rename norm_mul -> norm_mul_le; use norm_mul for the equality in normed fields; and norm_mul_le for the inequality in normed_rings

Estimated changes

Modified src/analysis/asymptotics.lean

Modified src/analysis/normed_space/basic.lean

modified theorem norm_mul

added theorem norm_mul_le

modified theorem norm_pow

added theorem norm_pow_le

added theorem norm_prod

deleted theorem normed_field.norm_pow

Modified src/data/complex/basic.lean

added theorem complex.abs_of_nat

Modified src/data/padics/padic_integers.lean