Skip to content
Snippets Groups Projects
Select Git revision
  • Subset
  • essais-8.18
  • master default protected
  • no_ms
  • pr_no_math-comp
  • released
  • test_skolem_ko
  • PhD_HM_2024
  • 1.0
  • Bochner.1.0
  • Tonelli.1.0
  • LInt_p.1.0
12 results
You can move around the graph by using the arrow keys.
Created with Raphaël 2.2.023Jan201918171613109612Dec986130Nov28252322212017161514111094331Oct2827252120191817161312109876543229Sep2826222120191716141397652131Aug302310Jul874130Jun292827242322212017161514131098732130May252423201918171614131211109ssr_Coquelicot and Coquelicot_ssr are no longer used.QUIET!Oups, now using SSReflect: have to force standard "rewrite" with "->".Move stuff around.Apparently, both conclusions of Steinitz exchange lemma are proved together·Borrow concat from sandbox (renamed concatF).ex_span -> span_ex.Highlight lemmas that are already explicitly used.Pas d'admits dans comb_linsimplify the proof of FE_is_unisolvant_cur lemma.Hint: @Sg E PE...Use magic: subst!Reorganize.Tune imports.Merge branch 'master' of depot.lipn.univ-paris13.fr:mayero/coq-num-analysisReorder + proof of compose_is_surj_compat, is_surj_compose andEssais SBReorganize + proof of compose_is_inj_compat and is_inj_compose (statement modified).Proof of compose_range_compat, compose_identity_compat, and compose_is_bij_id_compat.Reorder + proof of compose_is_bij_compat.Reorder + proof of is_bij_equiv.New section + proof of comb_lin_kronecker_product.Reorder + proof of comb_lin_scal_l (to be renamed).compose needs 3 sets -> new section.Merge branch 'master' of depot.lipn.univ-paris13.fr:mayero/coq-num-analysisWIP: comb_lin_ext_gen.Finish the proof of FE_is_unisolvant_cur lemma.Proof of FE_is_unisolvant_cur (WIP)remove is_linear_mapping_sigma_cur_aux lemma (not necessary).move and prove cur_to_ref_bij lemma.Add cur_to_ref_bij (admitted).Reorganization (= move stuff).Add is_bij_id_is_inj_is_surj_equiv and is_bij_is_inj_is_surj_equiv.Merge branch 'master' of https://www-lipn.univ-paris13.fr/coq-num-analysisProve cur_to_ref_inj and cur_to_ref_comp and ref_to_cur_compSuite de la réunion d'hier :Réunion 9/1Move a lot of lemmas!Finish proof of LagP1_is_affine.Add comb_lin_ext_minus_{l,r}.