mathlib3
31d28c62 - fix(src/algebra/big_operators/multiset): unify prod_le_pow_card and prod_le_of_forall_le (#12589)

Commit
3 years ago
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.
Author
Parents
Loading