Theorem IsNonarchimedean.finset_image_add

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) …
Modified IsNonarchimedean.finset_image_addView 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) …
Modified IsNonarchimedean.finset_image_addView on Github →
2025-03-27 09:53
Mathlib/Algebra/Order/Ring/IsNonarchimedean.lean
feat(Algebra/Order/Ring/IsNonarchimedean.lean): Nonarchimedean functions and APIs (#21963) …
Modified IsNonarchimedean.finset_image_addView on Github →
2024-10-21 14:44
Mathlib/Data/Real/IsNonarchimedean.lean
feat(Data/Real/IsNonarchimedean): add lemmas (#16767) …
Added IsNonarchimedean.finset_image_addView on Github →