Commit 2025-09-13 21:44 f459627d

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) This PR is similar to #28897 and I found a need for one of the added theorems in #29204. I've noticed that the existing theorem lcm_eq_zero_iff's rhs term 0 ∈ f '' s is not in simp normal form. Should this be deprecated and replaced? I have left comments about this in the code.