Theorem IsNonarchimedean.add_eq_max_of_ne'

Modification history

2026-08-16 13:11
Mathlib/Algebra/Order/Ring/IsNonarchimedean.lean
chore(Algebra/Order/Ring/IsNonarchimedean): remove FunLike hypotheses and generalize statements (#42408) …
Deleted IsNonarchimedean.add_eq_max_of_ne'View on Github →
2026-06-25 07:54
Mathlib/Algebra/Order/Ring/IsNonarchimedean.lean
chore: remove unused instances (#41013) …
Modified IsNonarchimedean.add_eq_max_of_ne'View on Github →
2026-06-17 10:37
Mathlib/Algebra/Order/Ring/IsNonarchimedean.lean
feat: lemmas towards showing gaussNorm on MvPowerSeries is an absolute value (#38049) …
Added IsNonarchimedean.add_eq_max_of_ne'View on Github →