Mathlib Changelog
Changelog
About
Github
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