Theorem IsNonarchimedean.add_eq_left_of_lt

Modification history

2025-03-27 09:53
Mathlib/Algebra/Order/Ring/IsNonarchimedean.lean
feat(Algebra/Order/Ring/IsNonarchimedean.lean): Nonarchimedean functions and APIs (#21963) …
Added IsNonarchimedean.add_eq_left_of_ltView on Github →