Theorem IsUltrametricDist.isUltrametricDist_of_forall_norm_natCast_le_one

Modification history

2024-10-20 19:39
Mathlib/Analysis/Normed/Field/Ultra.lean
feat(Analysis/Normed/Field/Ultra): nonarchimedean iff norm of nats le one (#15077)
Added IsUltrametricDist.isUltrametricDist_of_forall_norm_natCast_le_oneView on Github →