Theorem IsNonarchimedean.multiset_powerset_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.multiset_powerset_image_addView on Github →
2025-04-10 16:38
Mathlib/Algebra/Order/Ring/IsNonarchimedean.lean
chore: deprecate semibundled ordered algebraic typeclasses (#20676) …
Modified IsNonarchimedean.multiset_powerset_image_addView on Github →
2025-03-29 13:12
Mathlib/Algebra/Order/Ring/IsNonarchimedean.lean
feat(Algebra/Order/Ring/IsNonarchimedean): add powerset_image_add lemmas (#23253)
Added IsNonarchimedean.multiset_powerset_image_addView on Github →