mathlib3

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

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]. - [x] depends on: #16046