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.029Aug272630Jul292827262524221918171698428Jun2625212019181413111074314May13106129Apr282625242322212019152130Mar2928262522212019181615141310987654127Feb262322212019161514129876532131Jan30292827262524231817161527Dec232221201918171615141312118765432130Nov292827262423222120191716151413109réflexions ordres monomiauxordres monomiauxMOn_itemF_monotAdd type annotations.Typo...Fix the merge conflictMerge branch 'master' of https://www-lipn.univ-paris13.fr/coq-num-analysisSome minor modifsFix doubles.Some cleaning.Mv other results not needing commutativity of the scalar ring.Mv results not needing commutative ring.Generalize lm_basis_compat_equiv (bijS -> injS).Add documentation.Typos.Typo + new fixme!Merge branch 'master' of https://www-lipn.univ-paris13.fr/coq-num-analysisReorganize lemmasRename am_equiv -> am_lm_equiv,Simplify the proof of the lemma node_face0_in_Cdk.Reorganize Lemmas.typosSimplify the proofs of T_geom_face0_map_node and Slice_op_sum lemmas.Merge 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.