Commit 2023-10-17 20:58 75dfd25e

View on Github →

chore: rename Finset.powersetLen to powersetCard (#7667) I don't understand why this was ever named powersetLen, there isn't even the notion of the length of a Finset/Multiset.

Estimated changes

Modified Mathlib/Algebra/BigOperators/Basic.lean

added theorem Finset.prod_powersetCard

deleted theorem Finset.prod_powersetLen

Modified Mathlib/Algebra/BigOperators/Ring.lean

Modified Mathlib/Combinatorics/Additive/SalemSpencer.lean

Modified Mathlib/Combinatorics/SetFamily/LYM.lean

Modified Mathlib/Data/Finset/Powerset.lean

added theorem Finset.card_powersetCard

deleted theorem Finset.card_powersetLen

added theorem Finset.map_val_val_powersetCard

deleted theorem Finset.map_val_val_powersetLen

added theorem Finset.mem_powersetCard

deleted theorem Finset.mem_powersetLen

added theorem Finset.pairwise_disjoint_powersetCard

deleted theorem Finset.pairwise_disjoint_powersetLen

added def Finset.powersetCard

added theorem Finset.powersetCard_card_add

added theorem Finset.powersetCard_empty

added theorem Finset.powersetCard_eq_filter

added theorem Finset.powersetCard_map

added theorem Finset.powersetCard_mono

added theorem Finset.powersetCard_nonempty

added theorem Finset.powersetCard_self

added theorem Finset.powersetCard_succ_insert

added theorem Finset.powersetCard_sup

added theorem Finset.powersetCard_zero

deleted def Finset.powersetLen

deleted theorem Finset.powersetLen_card_add

deleted theorem Finset.powersetLen_empty

deleted theorem Finset.powersetLen_eq_filter

deleted theorem Finset.powersetLen_map

deleted theorem Finset.powersetLen_mono

deleted theorem Finset.powersetLen_nonempty

deleted theorem Finset.powersetLen_self

deleted theorem Finset.powersetLen_succ_insert

deleted theorem Finset.powersetLen_sup

deleted theorem Finset.powersetLen_zero

Modified Mathlib/Data/Finset/Slice.lean

added theorem Finset.subset_powersetCard_univ_iff

deleted theorem Finset.subset_powersetLen_univ_iff

added theorem Set.sized_powersetCard

deleted theorem Set.sized_powersetLen

Modified Mathlib/Data/Fintype/Powerset.lean

added theorem Finset.mem_powersetCard_univ

deleted theorem Finset.mem_powersetLen_univ

Modified Mathlib/Data/Multiset/Powerset.lean

added theorem Multiset.card_powersetCard

deleted theorem Multiset.card_powersetLen

added theorem Multiset.mem_powersetCard

added theorem Multiset.mem_powersetCardAux

deleted theorem Multiset.mem_powersetLen

deleted theorem Multiset.mem_powersetLenAux

added theorem Multiset.pairwise_disjoint_powersetCard

deleted theorem Multiset.pairwise_disjoint_powersetLen

added def Multiset.powersetCard

added def Multiset.powersetCardAux

added theorem Multiset.powersetCardAux_cons

added theorem Multiset.powersetCardAux_eq_map_coe

added theorem Multiset.powersetCardAux_nil

added theorem Multiset.powersetCardAux_perm

added theorem Multiset.powersetCardAux_zero

added theorem Multiset.powersetCard_card_add

added theorem Multiset.powersetCard_coe'

added theorem Multiset.powersetCard_coe

added theorem Multiset.powersetCard_cons

added theorem Multiset.powersetCard_empty

added theorem Multiset.powersetCard_le_powerset

added theorem Multiset.powersetCard_map

added theorem Multiset.powersetCard_mono

added theorem Multiset.powersetCard_zero_left

added theorem Multiset.powersetCard_zero_right

deleted def Multiset.powersetLen

deleted def Multiset.powersetLenAux

deleted theorem Multiset.powersetLenAux_cons

deleted theorem Multiset.powersetLenAux_eq_map_coe

deleted theorem Multiset.powersetLenAux_nil

deleted theorem Multiset.powersetLenAux_perm

deleted theorem Multiset.powersetLenAux_zero

deleted theorem Multiset.powersetLen_card_add

deleted theorem Multiset.powersetLen_coe'

deleted theorem Multiset.powersetLen_coe

deleted theorem Multiset.powersetLen_cons

deleted theorem Multiset.powersetLen_empty

deleted theorem Multiset.powersetLen_le_powerset

deleted theorem Multiset.powersetLen_map

deleted theorem Multiset.powersetLen_mono

deleted theorem Multiset.powersetLen_zero_left

deleted theorem Multiset.powersetLen_zero_right

Modified Mathlib/Data/Nat/Choose/Sum.lean

Modified Mathlib/RingTheory/MvPolynomial/NewtonIdentities.lean

Modified Mathlib/RingTheory/MvPolynomial/Symmetric.lean

Modified Mathlib/RingTheory/Polynomial/Vieta.lean

Modified Mathlib/Topology/Algebra/Polynomial.lean

Modified docs/100.yaml