Skip to content
Snippets Groups Projects

Repository graph

You can move around the graph by using the arrow keys.
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
Created with Raphaël 2.2.026Jun25212019181413111074314May13106129Apr282625242322212019152130Mar2928262522212019181615141310987654127Feb262322212019161514129876532131Jan30292827262524231817161527Dec232221201918171615141312118765432130Nov29282726242322212019171615141310987643231Oct302725Can't use here the vtx_cur from the context (lemma is used in the same section with another vtx_cur).Merge branch 'master' of depot.lipn.univ-paris13.fr:mayero/coq-num-analysisFinish doc.Unify doc.some refinementMerge branch 'master' of https://www-lipn.univ-paris13.fr/coq-num-analysisAdd some commentsrename variablesFix wrong Unix mode...WIP: add doc.Add doc.Tune doc.& -> /\.Mv ModuleSpace_R_compl.lc_lm_l to ModuleSpace_compl.Proof of lm_fct_scalF_l (previously fct_scalF_l_lm).dmit -> glop.few adjustmentsrearrange the lemma LagPd1_ref_surj.Rm now useless importSpecify resulting type.Add def compatible_sub."sub_struct HPT" becomes "sub PT" (with no algebra inside!)Doc.Rename compatible_as_* / *_compatible_as -> cas_* / *_casRename compatible_ms_* / *_compatible_ms -> cms_* / *_cmsRename compatible_r_* / *_compatible_r -> cr_* / *_crRename compatible_g_* / *_compatible_g -> cg_* / *_cgRename compatible_m_* / *_compatible_m -> cm_* / *_cmReplace unique_choice -> choiceF.Replace choice -> choiceF.We already have a witness, no need for choice to prove fun_from_empty_is_nonempty!Add choiceF (proved by induction, not using the general choice).Fix typo.Add pair_neq_spec.Simplify (= generalize) lemmas about (is_)unit_type.Merge branch 'master' of https://www-lipn.univ-paris13.fr/coq-num-analysisrewrite HL in one positionFix doc.preuve Sigma_LagPdk_cur_refRenommage + nettoyage FE_LagP avec k=0