Mathlib Changelog
v3
Changelog
About
Github
Mathlib v3 is deprecated.
Go to Mathlib v4
Commit
2020-07-13 19:01
2ae7ad81
View on Github →
feat(functor): definition multivariate functors (
#3360
) One part of
#3317
Estimated changes
Created
src/control/functor/multivariate.lean
added
theorem
mvfunctor.exists_iff_exists_of_mono
added
theorem
mvfunctor.id_map'
added
theorem
mvfunctor.id_map
added
def
mvfunctor.liftp'
added
def
mvfunctor.liftp
added
theorem
mvfunctor.liftp_def
added
theorem
mvfunctor.liftp_last_pred_iff
added
def
mvfunctor.liftr'
added
def
mvfunctor.liftr
added
theorem
mvfunctor.liftr_def
added
theorem
mvfunctor.liftr_last_rel_iff
added
theorem
mvfunctor.map_map
added
theorem
mvfunctor.of_mem_supp
added
def
mvfunctor.supp
Created
src/data/fin2.lean
added
def
fin2.add
added
def
fin2.elim0
added
def
fin2.insert_perm
added
def
fin2.left
added
def
fin2.of_nat'
added
def
fin2.opt_of_nat
added
def
fin2.remap_left
added
def
fin2.to_nat
added
inductive
fin2
Created
src/data/typevec.lean
added
def
typevec.append1
added
def
typevec.append1_cases
added
theorem
typevec.append1_cases_append1
added
theorem
typevec.append1_drop_last
added
def
typevec.append_fun
added
theorem
typevec.append_fun_aux
added
theorem
typevec.append_fun_comp'
added
theorem
typevec.append_fun_comp
added
theorem
typevec.append_fun_comp_id
added
theorem
typevec.append_fun_comp_split_fun
added
theorem
typevec.append_fun_id_id
added
theorem
typevec.append_fun_inj
added
theorem
typevec.append_prod_append_fun
added
def
typevec.arrow.mp
added
def
typevec.arrow.mpr
added
def
typevec.arrow
added
def
typevec.comp
added
theorem
typevec.comp_assoc
added
theorem
typevec.comp_id
added
theorem
typevec.const_append1
added
theorem
typevec.const_iff_true
added
theorem
typevec.const_nil
added
def
typevec.curry
added
def
typevec.diag_sub
added
theorem
typevec.diag_sub_val
added
def
typevec.drop
added
theorem
typevec.drop_append1'
added
theorem
typevec.drop_append1
added
def
typevec.drop_fun
added
theorem
typevec.drop_fun_append_fun
added
theorem
typevec.drop_fun_comp
added
theorem
typevec.drop_fun_split_fun
added
def
typevec.drop_repeat
added
theorem
typevec.eq_nil_fun
added
theorem
typevec.eq_of_drop_last_eq
added
theorem
typevec.fst_diag
added
theorem
typevec.fst_prod_mk
added
def
typevec.id
added
theorem
typevec.id_comp
added
theorem
typevec.id_eq_nil_fun
added
def
typevec.last
added
theorem
typevec.last_append1
added
def
typevec.last_fun
added
theorem
typevec.last_fun_append_fun
added
theorem
typevec.last_fun_comp
added
theorem
typevec.last_fun_split_fun
added
def
typevec.nil_fun
added
theorem
typevec.nil_fun_comp
added
def
typevec.of_repeat
added
def
typevec.of_subtype'
added
def
typevec.of_subtype
added
def
typevec.pred_last'
added
def
typevec.pred_last
added
def
typevec.prod.diag
added
def
typevec.prod.fst
added
def
typevec.prod.mk
added
def
typevec.prod.snd
added
def
typevec.prod
added
theorem
typevec.prod_id
added
def
typevec.rel_last'
added
def
typevec.rel_last
added
def
typevec.repeat
added
def
typevec.repeat_eq
added
theorem
typevec.repeat_eq_append1
added
theorem
typevec.repeat_eq_iff_eq
added
theorem
typevec.repeat_eq_nil
added
theorem
typevec.snd_diag
added
theorem
typevec.snd_prod_mk
added
theorem
typevec.split_drop_fun_last_fun
added
def
typevec.split_fun
added
theorem
typevec.split_fun_comp
added
theorem
typevec.split_fun_inj
added
def
typevec.subtype_
added
def
typevec.subtype_val
added
theorem
typevec.subtype_val_nil
added
def
typevec.to_append1_drop_last
added
def
typevec.to_subtype'
added
def
typevec.to_subtype
added
def
typevec.typevec_cases_cons₂
added
theorem
typevec.typevec_cases_cons₂_append_fun
added
def
typevec.typevec_cases_cons₃
added
def
typevec.typevec_cases_nil₂
added
theorem
typevec.typevec_cases_nil₂_append_fun
added
def
typevec.typevec_cases_nil₃
added
def
typevec
Modified
src/number_theory/dioph.lean
deleted
def
fin2.add
deleted
def
fin2.elim0
deleted
def
fin2.insert_perm
deleted
def
fin2.left
deleted
def
fin2.of_nat'
deleted
def
fin2.opt_of_nat
deleted
def
fin2.remap_left
deleted
def
fin2.to_nat
deleted
inductive
fin2