Commit 2022-08-17 00:31 e14ff257

feat(set_theory/cardinal): cardinality of multiset, polynomial and mv_polynomial (#15889)

• Show #(multiset α) = max (#α) ℵ₀ when α is nonempty. Show the same for #(α →₀ ℕ), which is used in the mv_polynomial proof (see below).
• Prove that the inequality in polynomial.cardinal_mk_le_max is an equality when the semiring is nontrivial. The result is no longer derived from the corresponding result for mv_polynomial to allow general semiring, not just comm_semiring.
• Generalize mv_polynomial.cardinal_mk_le_max to two possibly different universes, and prove that the inequality is an equality when the type of variables is nonempty and the semiring is nontrivial. W_type is no longer used so that part is removed from the file.
• Change the [encodable] assumption in mk_le_aleph_0 and mk_list_eq_aleph_0 to the weaker typeclass [countable].

• depends on: #16046