Theorem Multiset.subset_smul_self_of_ne_zero

Modification history

2026-06-26 12:41
Mathlib/Algebra/Order/Group/Multiset.lean
feat(Data/Nat): a number divides a power of its own radical (#40170) …
Added Multiset.subset_smul_self_of_ne_zeroView on Github →