Mathlib Changelog
v4
Changelog
About
Github
Commit
2025-03-29 13:12
dbd0b3b3
View on Github →
feat(Algebra/Order/Ring/IsNonarchimedean): add powerset_image_add lemmas (
#23253
)
Estimated changes
Modified
Mathlib/Algebra/Order/Ring/IsNonarchimedean.lean
added
theorem
IsNonarchimedean.finset_powerset_image_add
added
theorem
IsNonarchimedean.multiset_powerset_image_add