Commit 2025-03-27 09:53 924c191e
View on Github →feat(Algebra/Order/Ring/IsNonarchimedean.lean): Nonarchimedean functions and APIs (#21963)
We generalize the definition of nonarchimedean real-valued function to
def IsNonarchimedean {α : Type*} [Add α] (f : α → R) : Prop := ∀ a b : α, f (a + b) ≤ f a ⊔ f b
where R is any LinearOrderedSemiring R and some related APIs.