Commit 2024-08-11 18:43 22e0c3ba

View on Github →

chore: reduce Cardinal imports (#15579)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/MvPolynomial/Cardinal.lean

Modified Mathlib/Algebra/Polynomial/Cardinal.lean

Modified Mathlib/LinearAlgebra/Dimension/Free.lean

Modified Mathlib/SetTheory/Cardinal/Basic.lean

deleted theorem Cardinal.mk_finsupp_lift_of_fintype

deleted theorem Cardinal.mk_finsupp_of_fintype

Created Mathlib/SetTheory/Cardinal/Finsupp.lean

added theorem Cardinal.mk_finsupp_lift_of_fintype

added theorem Cardinal.mk_finsupp_lift_of_infinite'

added theorem Cardinal.mk_finsupp_lift_of_infinite

added theorem Cardinal.mk_finsupp_nat

added theorem Cardinal.mk_finsupp_of_fintype

added theorem Cardinal.mk_finsupp_of_infinite'

added theorem Cardinal.mk_finsupp_of_infinite

added theorem Cardinal.mk_multiset_of_countable

added theorem Cardinal.mk_multiset_of_infinite

added theorem Cardinal.mk_multiset_of_isEmpty

added theorem Cardinal.mk_multiset_of_nonempty

Modified Mathlib/SetTheory/Cardinal/Ordinal.lean

deleted theorem Cardinal.mk_finsupp_lift_of_infinite'

deleted theorem Cardinal.mk_finsupp_lift_of_infinite

deleted theorem Cardinal.mk_finsupp_nat

deleted theorem Cardinal.mk_finsupp_of_infinite'

deleted theorem Cardinal.mk_finsupp_of_infinite

deleted theorem Cardinal.mk_multiset_of_countable

deleted theorem Cardinal.mk_multiset_of_infinite

deleted theorem Cardinal.mk_multiset_of_isEmpty

deleted theorem Cardinal.mk_multiset_of_nonempty