mathlib

mathlib copied to clipboard

• 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

---

The part using W types can just be deleted. They were all just private definitions to prove the cardinality lemma.

bors d=vihdzp

:v: vihdzp can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

This PR/issue depends on:

• ~~leanprover-community/mathlib#16046~~ By Dependent Issues (🤖). Happy coding!

Is this PR ready now?

I think yes!

I planned to notify you once I confirm that CI passed, but you got here earlier than me :)

Then this looks alright to me now.

bors r+

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests