Commit 2024-10-20 19:39 a3996466

View on Github →

feat(Analysis/Normed/Field/Ultra): nonarchimedean iff norm of nats le one (#15077)

Estimated changes

Modified Mathlib.lean

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

added theorem IsUltrametricDist.isUltrametricDist_of_forall_norm_add_one_le_max_norm_one

added theorem IsUltrametricDist.isUltrametricDist_of_forall_norm_add_one_of_norm_le_one

added theorem IsUltrametricDist.isUltrametricDist_of_forall_norm_natCast_le_one

added theorem IsUltrametricDist.isUltrametricDist_of_forall_norm_sub_one_of_norm_le_one

added theorem IsUltrametricDist.isUltrametricDist_of_forall_pow_norm_le_nsmul_pow_max_one_norm