Commit 2023-12-26 23:40 c8b9760e

View on Github →

chore: deprecate prod_zero_iff_exists_zero (#9281)

  • Make Multiset.prod_eq_zero_iff a simp lemma.
  • Golf and deprecate prod_zero_iff_exists_zero; it was a bad API version of Multiset.prod_eq_zero_iff.
  • Make Ideal.mul_eq_bot a simp lemma`.
  • Add Ideal.multiset_prod_eq_bot (a simp lemma), deprecate Ideal.prod_eq_bot. The deprecated lemmas prod_zero_iff_exists_zero and Ideal.prod_eq_bot use ∃ x ∈ s, x = 0 instead of a simpler 0 ∈ s in the RHS.

Estimated changes