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