Theorem IsNonarchimedean.finset_image_add

Modification history

2024-10-21 14:44
Mathlib/Data/Real/IsNonarchimedean.lean
feat(Data/Real/IsNonarchimedean): add lemmas (#16767) …
Added IsNonarchimedean.finset_image_addView on Github →