Commit 2023-03-13 13:27 bb57ebcc

View on Github →

feat: port Analysis.Normed.Field.Basic (#2792)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Analysis/Normed/Field/Basic.lean

added theorem Filter.IsBoundedUnder_le.mul_tendsto_zero

added theorem Filter.Tendsto.zero_mul_isBoundedUnder_le

added theorem Filter.tendsto_mul_left_cobounded

added theorem Filter.tendsto_mul_right_cobounded

added theorem Finset.nnnorm_prod_le'

added theorem Finset.nnnorm_prod_le

added theorem Finset.norm_prod_le'

added theorem Finset.norm_prod_le

added theorem List.nnnorm_prod_le'

added theorem List.nnnorm_prod_le

added theorem List.norm_prod_le'

added theorem List.norm_prod_le

added theorem NNReal.nnnorm_eq

added theorem NNReal.norm_eq

added theorem Nat.norm_cast_le

added def NonUnitalNormedRing.induced

added def NonUnitalSeminormedRing.induced

added theorem NormOneClass.induced

added theorem NormOneClass.nontrivial

added theorem NormedAddCommGroup.tendsto_atTop'

added theorem NormedAddCommGroup.tendsto_atTop

added def NormedCommRing.induced

added def NormedDivisionRing.induced

added theorem NormedField.denseRange_nnnorm

added theorem NormedField.exists_lt_nnnorm_lt

added theorem NormedField.exists_lt_norm

added theorem NormedField.exists_lt_norm_lt

added theorem NormedField.exists_norm_lt

added theorem NormedField.exists_norm_lt_one

added theorem NormedField.exists_one_lt_norm

added def NormedField.induced

added theorem NormedField.nhdsWithin_isUnit_neBot

added theorem NormedField.punctured_nhds_neBot

added def NormedRing.induced

added theorem Real.nnnorm_mul_toNNReal

added theorem Real.toNNReal_mul_nnnorm

added def SeminormedCommRing.induced

added def SeminormedRing.induced

added theorem Units.nnnorm_pos

added theorem Units.norm_pos

added theorem dist_inv_inv₀

added theorem eventually_norm_pow_le

added theorem mulLeft_bound

added theorem mulRight_bound

added theorem nndist_inv_inv₀

added def nnnormHom

added theorem nnnorm_div

added theorem nnnorm_inv

added theorem nnnorm_mul

added theorem nnnorm_mul_le

added theorem nnnorm_norm

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 def normHom

added theorem norm_div

added theorem norm_inv

added theorem norm_map_one_of_pow_eq_one

added theorem norm_mul

added theorem norm_mul_le

added theorem norm_norm

added theorem norm_one_of_pow_eq_one

added theorem norm_pow

added theorem norm_pow_le'

added theorem norm_pow_le

added theorem norm_prod

added theorem norm_zpow

added theorem one_le_nnnorm_one

added theorem one_le_norm_one

Modified Mathlib/Analysis/Normed/Group/Basic.lean