Commit 2024-10-21 14:44 d2549910

View on Github →

feat(Data/Real/IsNonarchimedean): add lemmas (#16767) Used in #15373.

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/Order/Hom/Normed.lean

added theorem GroupNormClass.toNormedCommGroup_norm_eq

added theorem GroupNormClass.toNormedGroup_norm_eq

added theorem GroupSeminormClass.toSeminormedCommGroup_norm_eq

added theorem GroupSeminormClass.toSeminormedGroup_norm_eq

Created Mathlib/Algebra/Order/Hom/Ultra.lean

added theorem AddGroupSeminormClass.isUltrametricDist

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

added theorem IsUltrametricDist.exists_norm_finset_prod_le

added theorem IsUltrametricDist.exists_norm_finset_prod_le_of_nonempty

added theorem IsUltrametricDist.exists_norm_multiset_prod_le

Created Mathlib/Data/Real/IsNonarchimedean.lean

added theorem IsNonarchimedean.add_eq_max_of_ne

added theorem IsNonarchimedean.add_le

added theorem IsNonarchimedean.add_pow_le

added theorem IsNonarchimedean.finset_image_add

added theorem IsNonarchimedean.finset_image_add_of_nonempty

added theorem IsNonarchimedean.multiset_image_add

added theorem IsNonarchimedean.multiset_image_add_of_nonempty

added theorem IsNonarchimedean.nmul_le

added theorem IsNonarchimedean.nsmul_le