mathlib3

d6ce021f - feat(algebra/order/hom/basic): Non-archimedean homomorphisms (#16769)

feat(algebra/order/hom/basic): Non-archimedean homomorphisms (#16769) Define `nonarchimedean_hom_class `a general hom class for homs respecting `f (a + b) ≤ max (f a) (f b)`.