Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-06-30 23:04 7b0c1508

View on Github →

refactor(data/equiv): reorganize data.equiv deps

Estimated changes

Modified computability/primrec.lean

Modified data/array/lemmas.lean

added def equiv.array_equiv_fin

added def equiv.d_array_equiv_fin

Renamed data/equiv.lean to data/equiv/basic.lean

deleted def equiv.array_equiv_fin

deleted def equiv.bool_prod_nat_equiv_nat

deleted def equiv.d_array_equiv_fin

deleted def equiv.int_equiv_nat

deleted def equiv.nat_prod_nat_equiv_nat

deleted def equiv.nat_sum_bool_equiv_nat

deleted def equiv.nat_sum_nat_equiv_nat

deleted def equiv.prod_equiv_of_equiv_nat

deleted def equiv.vector_equiv_array

deleted def equiv.vector_equiv_fin

deleted theorem function.left_inverse.comp

deleted theorem function.left_inverse.f_g_eq_id

deleted theorem function.right_inverse.comp

deleted theorem function.right_inverse.g_f_eq_id

Created data/equiv/denumerable.lean

added theorem denumerable.decode_eq_of_nat

added theorem denumerable.decode_is_some

added theorem denumerable.encode_of_nat

added def denumerable.equiv₂

added def denumerable.eqv

added def denumerable.mk'

added def denumerable.of_equiv

added theorem denumerable.of_equiv_of_nat

added def denumerable.of_nat

added theorem denumerable.of_nat_encode

added theorem denumerable.of_nat_nat

added theorem denumerable.of_nat_of_decode

added def denumerable.pair

added theorem denumerable.prod_nat_of_nat

added theorem denumerable.prod_of_nat_val

added theorem denumerable.sigma_of_nat_val

Renamed data/encodable.lean to data/equiv/encodable.lean

deleted def encodable.decode_list

deleted theorem encodable.decode_list_succ

deleted theorem encodable.decode_list_zero

deleted def encodable.decode_multiset

deleted def encodable.encodable_of_list

deleted def encodable.encode_list

deleted theorem encodable.encode_list_cons

deleted theorem encodable.encode_list_nil

deleted def encodable.encode_multiset

deleted theorem encodable.length_le_encode

deleted def encodable.trunc_encodable_of_fintype

Renamed data/denumerable.lean to data/equiv/list.lean

deleted theorem denumerable.decode_eq_of_nat

deleted theorem denumerable.decode_is_some

deleted theorem denumerable.encode_of_nat

deleted def denumerable.equiv₂

deleted def denumerable.eqv

deleted def denumerable.mk'

deleted def denumerable.of_equiv

deleted theorem denumerable.of_equiv_of_nat

deleted def denumerable.of_nat

deleted theorem denumerable.of_nat_encode

deleted theorem denumerable.of_nat_nat

deleted theorem denumerable.of_nat_of_decode

deleted def denumerable.pair

deleted theorem denumerable.prod_nat_of_nat

deleted theorem denumerable.prod_of_nat_val

deleted theorem denumerable.sigma_of_nat_val

added def encodable.decode_list

added theorem encodable.decode_list_succ

added theorem encodable.decode_list_zero

added def encodable.decode_multiset

added def encodable.encodable_of_list

added def encodable.encode_list

added theorem encodable.encode_list_cons

added theorem encodable.encode_list_nil

added def encodable.encode_multiset

added theorem encodable.length_le_encode

added def encodable.trunc_encodable_of_fintype

Created data/equiv/nat.lean

added def equiv.bool_prod_nat_equiv_nat

added def equiv.int_equiv_nat

added def equiv.nat_prod_nat_equiv_nat

added def equiv.nat_sum_nat_equiv_nat

added def equiv.prod_equiv_of_equiv_nat

Modified data/erased.lean

Modified data/fintype.lean

Modified data/rat.lean

Modified data/real/cau_seq.lean

Modified data/set/basic.lean

added theorem set.image_congr

added theorem set.subtype_val_image

added theorem set.subtype_val_range

Modified data/set/countable.lean

Modified data/set/enumerate.lean

Modified data/set/lattice.lean

deleted theorem set.image_congr

deleted theorem set.subtype_val_image

deleted theorem set.subtype_val_range

Modified data/vector2.lean

added def equiv.vector_equiv_array

added def equiv.vector_equiv_fin

Modified group_theory/coset.lean

Modified group_theory/free_group.lean

Modified logic/embedding.lean

Modified logic/function.lean

added theorem function.left_inverse.comp

added theorem function.left_inverse.comp_eq_id

added theorem function.right_inverse.comp

added theorem function.right_inverse.comp_eq_id

Modified order/order_iso.lean