Skip to content
Snippets Groups Projects
Select Git revision
  • Subset
  • essais-8.18
  • master default protected
  • pr_no_math-comp
  • released
  • test_skolem_ko
  • PhD_HM_2024
  • 1.0
  • Bochner.1.0
  • Tonelli.1.0
  • LInt_p.1.0
11 results
You can move around the graph by using the arrow keys.
Created with Raphaël 2.2.022Jul1918171698428Jun2625212019181413111074314May13106129Apr282625242322212019152130Mar2928262522212019181615141310987654127Feb262322212019161514129876532131Jan30292827262524231817161527Dec232221201918171615141312118765432130Nov2928272624232221201917161514131098764Merge branch 'master' of https://www-lipn.univ-paris13.fr/coq-num-analysisAdd nat_plus_def, extF{,_zero}_ind_{l,r}, sum_def_R, sum_def_nat.Merge branch 'master' of https://www-lipn.univ-paris13.fr/coq-num-analysissimplify the lemma unisolvence_cur.MOn et grglexSome minor modificationsRéunion 17/7 (enlever affine_independant et k_pos) + lemmes sur MOnSimplification preuve Pd1_lin_span_LagPd1_curNo need for affine independence for k=0!Remove P1k_lin_span_LagP1k_cur_aux lemmaMaking some arguments implicit, others explicit.Add fct_cst_am, fct_point_of_as_am.Make nonemptyness witness O of sub_AffineSpace implicit.Some cleaning.Some simplifications of proofsMerge branch 'master' of depot.lipn.univ-paris13.fr:mayero/coq-num-analysisRename barycenter_* / *_barycenter -> baryc_* / *_baryc.- Remove T_geom_transports_node_aux, T_geom_inv_transports_node_aux lemmas.Can'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!)