Mathlib Changelog
v3
Changelog
About
Github
Mathlib v3 is deprecated.
Go to Mathlib v4
Commit
2017-09-08 14:49
8ef8f819
View on Github →
feat(data/equiv): port data/equiv.lean from Lean2
Estimated changes
Created
data/equiv.lean
added
theorem
equiv.apply_eq_iff_eq
added
theorem
equiv.apply_eq_iff_eq_inverse_apply
added
def
equiv.arrow_arrow_equiv_prod_arrow
added
def
equiv.arrow_congr
added
def
equiv.arrow_prod_equiv_prod_arrow
added
def
equiv.arrow_unit_equiv_unit
added
def
equiv.bool_equiv_unit_sum_unit
added
def
equiv.bool_prod_equiv_sum
added
theorem
equiv.comp_apply
added
def
equiv.decidable_eq_of_equiv
added
def
equiv.empty_arrow_equiv_unit
added
theorem
equiv.eq_iff_eq_of_injective
added
theorem
equiv.eq_of_to_fun_eq
added
def
equiv.false_arrow_equiv_unit
added
def
equiv.false_equiv_empty
added
def
equiv.fn
added
def
equiv.id
added
theorem
equiv.id_apply
added
def
equiv.inhabited_of_equiv
added
def
equiv.inv
added
theorem
equiv.inverse_apply_apply
added
def
equiv.nat_equiv_nat_sum_unit
added
def
equiv.nat_sum_bool_equiv_nat
added
def
equiv.nat_sum_unit_equiv_nat
added
def
equiv.perm
added
def
equiv.prod_assoc
added
def
equiv.prod_comm
added
def
equiv.prod_congr
added
def
equiv.prod_empty_left
added
def
equiv.prod_empty_right
added
def
equiv.prod_sum_distrib
added
def
equiv.prod_unit_left
added
def
equiv.prod_unit_right
added
def
equiv.subtype_equiv_of_subtype
added
def
equiv.sum_arrow_equiv_prod_arrow
added
def
equiv.sum_assoc
added
def
equiv.sum_comm
added
def
equiv.sum_congr
added
def
equiv.sum_empty_left
added
def
equiv.sum_empty_right
added
def
equiv.sum_prod_distrib
added
def
equiv.swap
added
theorem
equiv.swap_apply_def
added
theorem
equiv.swap_apply_left
added
theorem
equiv.swap_apply_of_ne_of_ne
added
theorem
equiv.swap_apply_right
added
theorem
equiv.swap_comm
added
theorem
equiv.swap_comp_apply
added
def
equiv.swap_core
added
theorem
equiv.swap_core_comm
added
theorem
equiv.swap_core_self
added
theorem
equiv.swap_core_swap_core
added
theorem
equiv.swap_self
added
theorem
equiv.swap_swap
added
def
equiv.unit_arrow_equiv
added
structure
equiv
added
theorem
function.left_inverse.f_g_eq_id
added
theorem
function.right_inverse.g_f_eq_id
added
def
subtype.map
added
theorem
subtype.map_comp
added
theorem
subtype.map_id