Theorem Multiset.ne_zero_iff_exists_mem

Modification history

2026-10-23 13:54
Mathlib/Data/Multiset/ZeroCons.lean
refactor(Algebra/Polynomial): improve characterisation of `p.roots = 0` (#44237) …
Added Multiset.ne_zero_iff_exists_memView on Github →