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.025Nov242321201918516Oct151087126Sep252423222120191817161513121110865429Aug272630Jul292827262524221918171698428Jun2625212019181413111074314May13106129Apr282625242322212019152130Mar2928262522212019181615141310987654127Feb262322212019161514129876532131Jan30292827262524231817161527Dec232221201918171615141312118765432130Nov292827262423Add equiv_rel_partial_equiv_rel,Mv stuff around.Fix defs using Matthias Ehrgott, 2005, Multicriteria Optimization!Function_compl:Mv stuff around.Propagate new API from Finite_family (new *lex).Remove *lex{T,F}.Add br_or_eq, br_and_neq, br_empty, br_universal, br_identity,Cosmetics.Add results.Spurious white.admit inside commentsPhD_HM_2024PhD_HM_2024Another known result.Rename asym_equiv -> asym_equiv_alt.Remove useless br_eq_or, br_neq_and.Add known results.essai sur lex pour ordres stricts/largesFix Div0 issue:Add nat_neq_0_equiv, nat_add_sub_{l,r}Ign notation incompatible prefix.FIXME: Div0 issue!WIP: migrate FEM to Coq-8.20.Context now needs a section.WIP: migrate Lebesgue for Coq-8.20.WIP: migrate Lebesgue for Coq-8.20.intuition -> auto with real/arith/zarithRlt_Rminus -> Rlt_0_minusRm unused Even requirement.Mv extF_widenF_S from Finite_family to ord_compl.Helper.Merge branch 'master' of depot.lipn.univ-paris13.fr:mayero/coq-num-analysisReorganize Compl.Add lex_1, colex_1.Add lex_1, colex_1.Fix doc.weighted orders, preuve de lexmodify the proof of unisolvence_cur.Change in indices.rename: node_cur_aux -> node_cur_alt.rename: