Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-11-18 03:59 c3019c79

View on Github →

refactor(data/fintype/basic): split file (#17578)

Estimated changes

Modified archive/100-theorems-list/73_ascending_descending_sequences.lean

Modified archive/imo/imo1987_q1.lean

Modified archive/imo/imo1994_q1.lean

Modified src/algebra/big_operators/basic.lean

Modified src/algebra/big_operators/fin.lean

Modified src/algebra/big_operators/pi.lean

Modified src/algebra/char_zero.lean

Modified src/algebra/group/conj.lean

Modified src/algebra/order/field/pi.lean

Modified src/algebra/order/field/power.lean

Modified src/algebra/order/nonneg/ring.lean

Modified src/algebra/ring/fin.lean

Modified src/analysis/complex/upper_half_plane/basic.lean

Modified src/category_theory/Fintype.lean

Modified src/category_theory/enriched/basic.lean

Modified src/category_theory/fin_category.lean

Modified src/category_theory/limits/concrete_category.lean

Modified src/category_theory/limits/constructions/limits_of_products_and_equalizers.lean

Modified src/category_theory/limits/lattice.lean

Modified src/category_theory/limits/shapes/finite_limits.lean

Modified src/combinatorics/configuration.lean

Modified src/combinatorics/derangements/finite.lean

Modified src/combinatorics/hales_jewett.lean

Modified src/combinatorics/set_family/harris_kleitman.lean

Modified src/combinatorics/set_family/intersecting.lean

Modified src/computability/DFA.lean

Modified src/computability/NFA.lean

Modified src/computability/turing_machine.lean

Modified src/data/dfinsupp/interval.lean

Modified src/data/fin/tuple/bubble_sort_induction.lean

Modified src/data/fin/tuple/sort.lean

Modified src/data/finite/basic.lean

Modified src/data/finite/set.lean

Modified src/data/finset/finsupp.lean

Modified src/data/finset/noncomm_prod.lean

Modified src/data/finset/pi_induction.lean

Modified src/data/finset/sort.lean

Modified src/data/finset/sym.lean

Modified src/data/fintype/basic.lean

deleted theorem card_finset_fin_le

deleted theorem card_perms_of_finset

deleted def equiv.of_left_inverse_of_card_le

deleted def equiv.of_right_inverse_of_card_le

deleted theorem fin.cast_eq_cast'

deleted theorem fin.equiv_iff_eq

deleted theorem fin_injective

deleted theorem finite.exists_infinite_fiber

deleted theorem finite.exists_max

deleted theorem finite.exists_min

deleted theorem finite.exists_ne_map_eq_of_infinite

deleted theorem finite.exists_univ_list

deleted theorem finite.induction_empty_option

deleted theorem finite.injective_iff_bijective

deleted theorem finite.injective_iff_surjective

deleted theorem finite.injective_iff_surjective_of_equiv

deleted theorem finite.of_injective

deleted theorem finite.of_surjective

deleted theorem finite.preorder.well_founded_gt

deleted theorem finite.preorder.well_founded_lt

deleted theorem finite.surjective_iff_bijective

deleted theorem finite.well_founded_of_trans_of_irrefl

deleted theorem finite_iff_nonempty_fintype

deleted theorem finset.card_compl

deleted theorem finset.card_compl_lt_iff_nonempty

deleted theorem finset.card_eq_iff_eq_univ

deleted theorem finset.card_fin

deleted theorem finset.card_le_univ

deleted theorem finset.card_lt_iff_ne_univ

deleted theorem finset.card_lt_univ_of_not_mem

deleted theorem finset.card_univ

deleted theorem finset.card_univ_diff

deleted theorem finset.eq_univ_of_card

deleted theorem finset.exists_equiv_extend_of_card_eq

deleted theorem finset.exists_maximal

deleted theorem finset.exists_minimal

deleted theorem finset.fold_inf_univ

deleted theorem finset.fold_sup_univ

deleted theorem finset.inf_univ_eq_infi

deleted theorem finset.mem_powerset_len_univ_iff

deleted theorem finset.powerset_eq_univ

deleted theorem finset.powerset_univ

deleted theorem finset.sup_univ_eq_supr

deleted theorem finset.univ_disj_sum_univ

deleted theorem finset.univ_filter_card_eq

deleted theorem finset.univ_map_embedding

deleted theorem finset.univ_pi_univ

deleted theorem finset.univ_product_univ

deleted theorem finset.univ_sigma_univ

deleted theorem fintype.bijective_iff_injective_and_card

deleted theorem fintype.bijective_iff_surjective_and_card

deleted def fintype.card

deleted theorem fintype.card_Prop

deleted theorem fintype.card_bool

deleted theorem fintype.card_coe

deleted theorem fintype.card_compl_eq_card_compl

deleted theorem fintype.card_compl_set

deleted theorem fintype.card_congr'

deleted theorem fintype.card_congr

deleted theorem fintype.card_empty

deleted theorem fintype.card_eq

deleted theorem fintype.card_eq_one_iff

deleted theorem fintype.card_eq_one_iff_nonempty_unique

deleted theorem fintype.card_eq_one_of_forall_eq

deleted theorem fintype.card_eq_zero

deleted def fintype.card_eq_zero_equiv_equiv_empty

deleted theorem fintype.card_eq_zero_iff

deleted theorem fintype.card_equiv

deleted theorem fintype.card_fin

deleted theorem fintype.card_fin_even

deleted theorem fintype.card_finset

deleted theorem fintype.card_finset_len

deleted theorem fintype.card_le_of_embedding

deleted theorem fintype.card_le_of_injective

deleted theorem fintype.card_le_of_surjective

deleted theorem fintype.card_le_one_iff

deleted theorem fintype.card_le_one_iff_subsingleton

deleted theorem fintype.card_lex

deleted theorem fintype.card_lt_of_injective_not_surjective

deleted theorem fintype.card_lt_of_injective_of_not_mem

deleted theorem fintype.card_lt_of_surjective_not_injective

deleted theorem fintype.card_ne_zero

deleted theorem fintype.card_of_bijective

deleted theorem fintype.card_of_finset'

deleted theorem fintype.card_of_finset

deleted theorem fintype.card_of_is_empty

deleted theorem fintype.card_of_subsingleton

deleted theorem fintype.card_of_subtype

deleted theorem fintype.card_option

deleted theorem fintype.card_order_dual

deleted theorem fintype.card_pempty

deleted theorem fintype.card_perm

deleted theorem fintype.card_plift

deleted theorem fintype.card_pos

deleted theorem fintype.card_pos_iff

deleted theorem fintype.card_prod

deleted theorem fintype.card_punit

deleted theorem fintype.card_quotient_le

deleted theorem fintype.card_quotient_lt

deleted theorem fintype.card_range

deleted theorem fintype.card_range_le

deleted theorem fintype.card_set

deleted theorem fintype.card_subtype

deleted theorem fintype.card_subtype_compl

deleted theorem fintype.card_subtype_eq'

deleted theorem fintype.card_subtype_eq

deleted theorem fintype.card_subtype_le

deleted theorem fintype.card_subtype_lt

deleted theorem fintype.card_subtype_mono

deleted theorem fintype.card_subtype_or

deleted theorem fintype.card_subtype_or_disjoint

deleted theorem fintype.card_sum

deleted theorem fintype.card_ulift

deleted theorem fintype.card_unique

deleted theorem fintype.card_unit

deleted theorem fintype.card_units

deleted theorem fintype.card_units_int

deleted theorem fintype.coe_pi_finset

deleted theorem fintype.exists_ne_map_eq_of_card_lt

deleted theorem fintype.exists_ne_of_one_lt_card

deleted theorem fintype.exists_pair_of_one_lt_card

deleted theorem fintype.induction_empty_option

deleted theorem fintype.induction_subsingleton_or_nontrivial

deleted theorem fintype.mem_pi_finset

deleted theorem fintype.of_equiv_card

deleted theorem fintype.one_lt_card

deleted theorem fintype.one_lt_card_iff

deleted theorem fintype.one_lt_card_iff_nontrivial

deleted def fintype.pi_finset

deleted theorem fintype.pi_finset_disjoint_of_disjoint

deleted theorem fintype.pi_finset_empty

deleted theorem fintype.pi_finset_singleton

deleted theorem fintype.pi_finset_subset

deleted theorem fintype.pi_finset_subsingleton

deleted theorem fintype.pi_finset_univ

deleted theorem fintype.subtype_card

deleted def fintype.trunc_equiv_fin

deleted def fintype.trunc_equiv_fin_of_card_eq

deleted def fintype.trunc_equiv_of_card_eq

deleted def fintype.trunc_fin_bijection

deleted def fintype.trunc_rec_empty_option

deleted theorem fintype.two_lt_card_iff

deleted def fintype_of_fintype_ne

deleted def fintype_of_option

deleted def fintype_of_option_equiv

deleted def fintype_perm

deleted theorem function.embedding.equiv_of_fintype_self_embedding_to_embedding

deleted theorem function.embedding.exists_of_card_le_finset

deleted theorem function.embedding.is_empty_of_card_lt

deleted theorem function.embedding.nonempty_iff_card_le

deleted theorem function.embedding.nonempty_of_card_le

deleted def function.embedding.trunc_of_card_le

deleted theorem function.left_inverse.right_inverse_of_card_le

deleted theorem function.right_inverse.left_inverse_of_card_le

deleted theorem image_subtype_ne_univ_eq_image_erase

deleted theorem image_subtype_univ_ssubset_image_univ

deleted theorem infinite.exists_not_mem_finset

deleted theorem infinite.exists_subset_card_eq

deleted theorem infinite.exists_superset_card_eq

deleted theorem infinite.of_injective

deleted theorem infinite.of_injective_to_set

deleted theorem infinite.of_not_fintype

deleted theorem infinite.of_surjective

deleted theorem infinite.of_surjective_from_set

deleted theorem infinite_prod

deleted theorem infinite_sum

deleted theorem is_empty_fintype

deleted theorem length_perms_of_list

deleted theorem list.nodup.length_le_card

deleted theorem mem_of_mem_perms_of_list

deleted theorem mem_perms_of_finset_iff

deleted theorem mem_perms_of_list_iff

deleted theorem mem_perms_of_list_of_mem

deleted theorem nodup_perms_of_list

deleted theorem nonempty_fintype

deleted theorem not_injective_infinite_finite

deleted theorem not_surjective_finite_infinite

deleted def perms_of_finset

deleted def perms_of_list

deleted theorem pi.infinite_of_exists_right

deleted theorem set.maps_to.exists_equiv_extend_of_card_eq

deleted theorem set.to_finset_card

deleted theorem set.to_finset_off_diag

deleted theorem set.to_finset_prod

deleted theorem set_fintype_card_eq_univ_iff

deleted theorem set_fintype_card_le_univ

deleted def trunc_of_card_pos

deleted theorem units_int.univ

deleted theorem univ_eq_singleton_of_card_one

deleted theorem univ_option

Created src/data/fintype/big_operators.lean

added theorem card_vector

added theorem equiv.prod_comp'

added theorem equiv.prod_comp

added theorem fin.prod_univ_eq_prod_range

added theorem finset.card_pi

added theorem finset.prod_attach_univ

added theorem finset.prod_fiberwise

added theorem finset.prod_fin_eq_prod_range

added theorem finset.prod_to_finset_eq_subtype

added theorem finset.prod_univ_pi

added theorem finset.prod_univ_sum

added theorem fintype.card_eq_sum_ones

added theorem fintype.card_fun

added theorem fintype.card_pi

added theorem fintype.card_pi_finset

added theorem fintype.card_sigma

added theorem fintype.eq_of_subsingleton_of_prod_eq

added theorem fintype.prod_bool

added theorem fintype.prod_congr

added theorem fintype.prod_dite

added theorem fintype.prod_eq_mul

added theorem fintype.prod_eq_one

added theorem fintype.prod_eq_single

added theorem fintype.prod_extend_by_one

added theorem fintype.prod_fiberwise

added theorem fintype.prod_option

added theorem fintype.prod_sum_elim

added theorem fintype.prod_sum_type

added theorem fintype.sum_pow_mul_eq_add_pow

added theorem function.bijective.prod_comp

Modified src/data/fintype/card.lean

added theorem card_finset_fin_le

deleted theorem card_vector

added def equiv.of_left_inverse_of_card_le

added def equiv.of_right_inverse_of_card_le

deleted theorem equiv.prod_comp'

deleted theorem equiv.prod_comp

added theorem fin.cast_eq_cast'

added theorem fin.equiv_iff_eq

deleted theorem fin.prod_univ_eq_prod_range

added theorem fin_injective

added theorem finite.exists_infinite_fiber

added theorem finite.exists_ne_map_eq_of_infinite

added theorem finite.exists_univ_list

added theorem finite.injective_iff_bijective

added theorem finite.injective_iff_surjective

added theorem finite.injective_iff_surjective_of_equiv

added theorem finite.of_injective

added theorem finite.of_surjective

added theorem finite.preorder.well_founded_gt

added theorem finite.preorder.well_founded_lt

added theorem finite.surjective_iff_bijective

added theorem finite.well_founded_of_trans_of_irrefl

added theorem finite_iff_nonempty_fintype

added theorem finset.card_compl

added theorem finset.card_compl_lt_iff_nonempty

added theorem finset.card_eq_iff_eq_univ

added theorem finset.card_fin

added theorem finset.card_le_univ

added theorem finset.card_lt_iff_ne_univ

added theorem finset.card_lt_univ_of_not_mem

deleted theorem finset.card_pi

added theorem finset.card_univ

added theorem finset.card_univ_diff

added theorem finset.eq_univ_of_card

added theorem finset.exists_maximal

added theorem finset.exists_minimal

deleted theorem finset.prod_attach_univ

deleted theorem finset.prod_fiberwise

deleted theorem finset.prod_fin_eq_prod_range

deleted theorem finset.prod_to_finset_eq_subtype

deleted theorem finset.prod_univ_pi

deleted theorem finset.prod_univ_sum

added theorem finset.univ_map_embedding

added theorem fintype.bijective_iff_injective_and_card

added theorem fintype.bijective_iff_surjective_and_card

added def fintype.card

added theorem fintype.card_Prop

added theorem fintype.card_bool

added theorem fintype.card_coe

added theorem fintype.card_compl_eq_card_compl

added theorem fintype.card_compl_set

added theorem fintype.card_congr'

added theorem fintype.card_congr

added theorem fintype.card_empty

added theorem fintype.card_eq

added theorem fintype.card_eq_one_iff

added theorem fintype.card_eq_one_iff_nonempty_unique

added theorem fintype.card_eq_one_of_forall_eq

deleted theorem fintype.card_eq_sum_ones

added theorem fintype.card_eq_zero

added def fintype.card_eq_zero_equiv_equiv_empty

added theorem fintype.card_eq_zero_iff

added theorem fintype.card_fin

deleted theorem fintype.card_fun

added theorem fintype.card_le_of_embedding

added theorem fintype.card_le_of_injective

added theorem fintype.card_le_of_surjective

added theorem fintype.card_le_one_iff

added theorem fintype.card_le_one_iff_subsingleton

added theorem fintype.card_lex

added theorem fintype.card_lt_of_injective_not_surjective

added theorem fintype.card_lt_of_injective_of_not_mem

added theorem fintype.card_lt_of_surjective_not_injective

added theorem fintype.card_ne_zero

added theorem fintype.card_of_bijective

added theorem fintype.card_of_finset'

added theorem fintype.card_of_finset

added theorem fintype.card_of_is_empty

added theorem fintype.card_of_subsingleton

added theorem fintype.card_of_subtype

added theorem fintype.card_order_dual

added theorem fintype.card_pempty

deleted theorem fintype.card_pi

deleted theorem fintype.card_pi_finset

added theorem fintype.card_plift

added theorem fintype.card_pos

added theorem fintype.card_pos_iff

added theorem fintype.card_punit

added theorem fintype.card_quotient_le

added theorem fintype.card_quotient_lt

added theorem fintype.card_range

added theorem fintype.card_range_le

deleted theorem fintype.card_sigma

added theorem fintype.card_subtype

added theorem fintype.card_subtype_compl

added theorem fintype.card_subtype_eq'

added theorem fintype.card_subtype_eq

added theorem fintype.card_subtype_le

added theorem fintype.card_subtype_lt

added theorem fintype.card_subtype_mono

added theorem fintype.card_ulift

added theorem fintype.card_unique

added theorem fintype.card_unit

deleted theorem fintype.eq_of_subsingleton_of_prod_eq

added theorem fintype.exists_ne_map_eq_of_card_lt

added theorem fintype.exists_ne_of_one_lt_card

added theorem fintype.exists_pair_of_one_lt_card

added theorem fintype.induction_subsingleton_or_nontrivial

added theorem fintype.of_equiv_card

added theorem fintype.one_lt_card

added theorem fintype.one_lt_card_iff

added theorem fintype.one_lt_card_iff_nontrivial

deleted theorem fintype.prod_bool

deleted theorem fintype.prod_congr

deleted theorem fintype.prod_dite

deleted theorem fintype.prod_eq_mul

deleted theorem fintype.prod_eq_one

deleted theorem fintype.prod_eq_single

deleted theorem fintype.prod_extend_by_one

deleted theorem fintype.prod_fiberwise

deleted theorem fintype.prod_option

deleted theorem fintype.prod_sum_elim

deleted theorem fintype.prod_sum_type

added theorem fintype.subtype_card

deleted theorem fintype.sum_pow_mul_eq_add_pow

added def fintype.trunc_equiv_fin

added def fintype.trunc_equiv_fin_of_card_eq

added def fintype.trunc_equiv_of_card_eq

added def fintype.trunc_fin_bijection

added theorem fintype.two_lt_card_iff

deleted theorem function.bijective.prod_comp

added theorem function.embedding.equiv_of_fintype_self_embedding_to_embedding

added theorem function.embedding.exists_of_card_le_finset

added theorem function.embedding.is_empty_of_card_lt

added theorem function.embedding.nonempty_iff_card_le

added theorem function.embedding.nonempty_of_card_le

added def function.embedding.trunc_of_card_le

added theorem function.left_inverse.right_inverse_of_card_le

added theorem function.right_inverse.left_inverse_of_card_le

added theorem infinite.exists_not_mem_finset

added theorem infinite.exists_subset_card_eq

added theorem infinite.exists_superset_card_eq

added theorem infinite.of_injective

added theorem infinite.of_injective_to_set

added theorem infinite.of_not_fintype

added theorem infinite.of_surjective

added theorem infinite.of_surjective_from_set

added theorem is_empty_fintype

added theorem list.nodup.length_le_card

added theorem nonempty_fintype

added theorem not_injective_infinite_finite

added theorem not_surjective_finite_infinite

added theorem set.to_finset_card

added theorem set_fintype_card_eq_univ_iff

added theorem set_fintype_card_le_univ

added def trunc_of_card_pos

added theorem univ_eq_singleton_of_card_one

Modified src/data/fintype/card_embedding.lean

Created src/data/fintype/lattice.lean

added theorem finite.exists_max

added theorem finite.exists_min

added theorem finset.fold_inf_univ

added theorem finset.fold_sup_univ

added theorem finset.inf_univ_eq_infi

added theorem finset.sup_univ_eq_supr

Modified src/data/fintype/list.lean

Created src/data/fintype/option.lean

added theorem finite.induction_empty_option

added theorem fintype.card_option

added theorem fintype.induction_empty_option

added def fintype.trunc_rec_empty_option

added def fintype_of_option

added def fintype_of_option_equiv

added theorem univ_option

Modified src/data/fintype/order.lean

Created src/data/fintype/parity.lean

added theorem fintype.card_fin_even

Created src/data/fintype/perm.lean

added theorem card_perms_of_finset

added theorem fintype.card_equiv

added theorem fintype.card_perm

added def fintype_perm

added theorem length_perms_of_list

added theorem mem_of_mem_perms_of_list

added theorem mem_perms_of_finset_iff

added theorem mem_perms_of_list_iff

added theorem mem_perms_of_list_of_mem

added theorem nodup_perms_of_list

added def perms_of_finset

added def perms_of_list

Created src/data/fintype/pi.lean

added theorem finset.univ_pi_univ

added theorem fintype.coe_pi_finset

added theorem fintype.mem_pi_finset

added def fintype.pi_finset

added theorem fintype.pi_finset_disjoint_of_disjoint

added theorem fintype.pi_finset_empty

added theorem fintype.pi_finset_singleton

added theorem fintype.pi_finset_subset

added theorem fintype.pi_finset_subsingleton

added theorem fintype.pi_finset_univ

Created src/data/fintype/powerset.lean

added theorem finset.mem_powerset_len_univ_iff

added theorem finset.powerset_eq_univ

added theorem finset.powerset_univ

added theorem finset.univ_filter_card_eq

added theorem fintype.card_finset

added theorem fintype.card_finset_len

added theorem fintype.card_set

Created src/data/fintype/prod.lean

added theorem finset.univ_product_univ

added theorem fintype.card_prod

added theorem infinite_prod

added theorem pi.infinite_of_exists_right

added theorem set.to_finset_off_diag

added theorem set.to_finset_prod

Created src/data/fintype/sigma.lean

added theorem finset.univ_sigma_univ

Modified src/data/fintype/small.lean

Created src/data/fintype/sum.lean

added theorem finset.exists_equiv_extend_of_card_eq

added theorem finset.univ_disj_sum_univ

added theorem fintype.card_subtype_or

added theorem fintype.card_subtype_or_disjoint

added theorem fintype.card_sum

added def fintype_of_fintype_ne

added theorem image_subtype_ne_univ_eq_image_erase

added theorem image_subtype_univ_ssubset_image_univ

added theorem infinite_sum

added theorem set.maps_to.exists_equiv_extend_of_card_eq

Created src/data/fintype/units.lean

added theorem fintype.card_units

added theorem fintype.card_units_int

added theorem units_int.univ

Created src/data/fintype/vector.lean

Modified src/data/int/absolute_value.lean

Modified src/data/matrix/basic.lean

Modified src/data/multiset/fintype.lean

Modified src/data/nat/digits.lean

Modified src/data/nat/fib.lean

Modified src/data/nat/prime.lean

Modified src/data/pi/interval.lean

Modified src/data/polynomial/degree/definitions.lean

Modified src/data/set_like/fintype.lean

Modified src/data/sign.lean

Modified src/data/sym/card.lean

Modified src/data/zmod/defs.lean

Modified src/group_theory/group_action/quotient.lean

Modified src/group_theory/noncomm_pi_coprod.lean

Modified src/group_theory/perm/cycle/basic.lean

Modified src/group_theory/perm/option.lean

Modified src/group_theory/perm/subgroup.lean

Modified src/group_theory/subsemigroup/centralizer.lean

Modified src/linear_algebra/basis.lean

Modified src/linear_algebra/matrix/determinant.lean

Modified src/linear_algebra/multilinear/basic.lean

Modified src/logic/denumerable.lean

Modified src/logic/equiv/list.lean

Modified src/number_theory/bernoulli.lean

Modified src/number_theory/legendre_symbol/quadratic_char.lean

Modified src/number_theory/sum_four_squares.lean

Modified src/order/category/FinBoolAlg.lean

Modified src/order/jordan_holder.lean

Modified src/order/sup_indep.lean

Modified src/ring_theory/fintype.lean

Modified src/ring_theory/witt_vector/witt_polynomial.lean

Modified src/set_theory/cardinal/basic.lean

Modified src/topology/alexandroff.lean

Modified test/derive_fintype.lean