Mathlib Changelog
v4
Changelog
About
Github
Theorem
IsNonarchimedean.add_eq_max_of_ne
Modification history
2024-10-21 14:44
Mathlib/Data/Real/IsNonarchimedean.lean
feat(Data/Real/IsNonarchimedean): add lemmas (#16767) …
Added
IsNonarchimedean.add_eq_max_of_ne
View on Github →