Commit 2022-03-12 11:37 31d28c62

fix(src/algebra/big_operators/multiset): unify prod_le_pow_card and prod_le_of_forall_le (#12589) using the name prod_le_pow_card as per https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/duplicate.20lemmas but use the phrasing of prod_le_of_forall_le with non-implicit multiset, as that is how it is used.