Theorem Multiset.lcm_ne_zero_iff

Modification history

2025-09-13 21:44
Mathlib/Algebra/GCDMonoid/Multiset.lean
feat(Algebra/GCDMonoid/Finset): change the signature of `lcm_eq_zero_iff` to its simp normal form and add `lcm_ne_zero_iff` theorems (#29208) …
Added Multiset.lcm_ne_zero_iffView on Github →