Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-03-02 21:08 ce26d75d

View on Github →

refactor(analysis/normed_space/basic): split into normed_space and ../normed/normed_field (#12410) Splits off the sections about normed rings and fields of the file analysis/normed_space/basic into a new file analysis/normed/normed_field.

Estimated changes

added theorem eventually_norm_pow_le
added theorem finset.norm_prod_le'
added theorem finset.norm_prod_le
added theorem int.norm_cast_rat
added theorem int.norm_cast_real
added theorem int.norm_eq_abs
added theorem list.norm_prod_le'
added theorem list.norm_prod_le
added theorem mul_left_bound
added theorem mul_right_bound
added theorem nnnorm_div
added def nnnorm_hom
added theorem nnnorm_inv
added theorem nnnorm_mul
added theorem nnnorm_mul_le
added theorem nnnorm_norm
added theorem nnnorm_nsmul_le
added theorem nnnorm_one
added theorem nnnorm_pow
added theorem nnnorm_pow_le'
added theorem nnnorm_pow_le
added theorem nnnorm_prod
added theorem nnnorm_zpow
added theorem nnnorm_zsmul_le
added theorem nnreal.coe_nat_abs
added theorem nnreal.nnnorm_eq
added theorem nnreal.norm_eq
added theorem norm_div
added def norm_hom
added theorem norm_inv
added theorem norm_matrix_le_iff
added theorem norm_matrix_lt_iff
added theorem norm_mul
added theorem norm_mul_le
added theorem norm_norm
added theorem norm_nsmul_le
added theorem norm_pow
added theorem norm_pow_le'
added theorem norm_pow_le
added theorem norm_prod
added theorem norm_zpow
added theorem norm_zsmul_le
added theorem rat.norm_cast_real
added theorem real.nnnorm_coe_nat
added theorem real.nnnorm_of_nonneg
added theorem real.nnnorm_two
added theorem real.norm_coe_nat
added theorem real.norm_of_nonneg
added theorem real.norm_of_nonpos
added theorem real.norm_two
added theorem summable.mul_norm
added theorem summable.mul_of_nonneg
added theorem units.norm_pos
deleted theorem eventually_norm_pow_le
deleted theorem finset.norm_prod_le'
deleted theorem finset.norm_prod_le
deleted theorem int.norm_cast_rat
deleted theorem int.norm_cast_real
deleted theorem int.norm_eq_abs
deleted theorem list.norm_prod_le'
deleted theorem list.norm_prod_le
deleted def matrix.normed_group
deleted theorem mul_left_bound
deleted theorem mul_right_bound
deleted theorem nnnorm_div
deleted def nnnorm_hom
deleted theorem nnnorm_inv
deleted theorem nnnorm_mul
deleted theorem nnnorm_mul_le
deleted theorem nnnorm_norm
deleted theorem nnnorm_nsmul_le
deleted theorem nnnorm_one
deleted theorem nnnorm_pow
deleted theorem nnnorm_pow_le'
deleted theorem nnnorm_pow_le
deleted theorem nnnorm_prod
deleted theorem nnnorm_zpow
deleted theorem nnnorm_zsmul_le
deleted theorem nnreal.coe_nat_abs
deleted theorem nnreal.nnnorm_eq
deleted theorem nnreal.norm_eq
deleted theorem norm_div
deleted def norm_hom
deleted theorem norm_inv
deleted theorem norm_matrix_le_iff
deleted theorem norm_matrix_lt_iff
deleted theorem norm_mul
deleted theorem norm_mul_le
deleted theorem norm_norm
deleted theorem norm_nsmul_le
deleted theorem norm_pow
deleted theorem norm_pow_le'
deleted theorem norm_pow_le
deleted theorem norm_prod
deleted theorem norm_zpow
deleted theorem norm_zsmul_le
deleted theorem rat.norm_cast_real
deleted theorem real.ennnorm_eq_of_real
deleted theorem real.nnnorm_coe_nat
deleted theorem real.nnnorm_of_nonneg
deleted theorem real.nnnorm_two
deleted theorem real.norm_coe_nat
deleted theorem real.norm_of_nonneg
deleted theorem real.norm_of_nonpos
deleted theorem real.norm_two
deleted theorem real.of_real_le_ennnorm
deleted theorem summable.mul_norm
deleted theorem summable.mul_of_nonneg
deleted theorem units.norm_pos