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.018Oct171614131211109653229Sep282726252221201918171514131211876542131Aug30292827242321181716151312111087643231Jul2827262524212019181713121098765430Jun2827262322212019161514131298765131May30262524232220171615141211109543229Apr2827262422212019181714131211765ord_compl, Finite_family, Monoid_compl, Finite_dim:poly_Lagrange, FE_simplex:Replace 'R_ModuleSpace^d with fct_ModuleSpace.ModuleSpace_compl:updated; next: for poly_lagrangeImport multi_index.vDeplacer les multi-index dans un nouveau fichier.WIP P_approx_k_d_monotoneIt compiles !Add vtx_cur_1_neq, T_geom_k_1, T_geom_inv_k_1, LagPk_1_cur_eq.Modify T_geom_transports_convex lemma.Minor cleaning in LM/compatible.vClean up in proofs of LM/logic_tricksMerge branch 'master' of depot.lipn.univ-paris13.fr:mayero/coq-num-analysisnat_compl:Merge branch 'master' of https://www-lipn.univ-paris13.fr/coq-num-analysisProve LagP1_d_ref_neq0_liftF_S_aux, sum_le_R, sum_constF_R,revert poly_Lagrange.vajout dans poly_Lagrange pour réparer une preuveMerge branch 'master' of https://www-lipn.univ-paris13.fr/coq-num-analysisAdd and prove minus_plus_equiv, LagP1_d_ref_liftF_SUn peu de ménage dans LM/R_compl.vProve Phi_is_affine_mapping, Phi_eq2.ménage sur polynômes génériques + qq preuves Pkd_multchg def, trivial factsMerge branch 'master' of https://www-lipn.univ-paris13.fr/coq-num-analysis- Prove FE_LagPk_d_ref_is_unisolvent.Réunion 11 octobre : multiplication de polynômesWIP: filterP_cast_ord.Merge branch 'master' of depot.lipn.univ-paris13.fr:mayero/coq-num-analysisProofs of lenPF0_alt, lenPFmax_alt, lenPF_cast_ord.Merge branch 'master' of https://www-lipn.univ-paris13.fr/coq-num-analysis- Rearrange items.ord_compl:Finite_family:Merge branch 'master' of depot.lipn.univ-paris13.fr:mayero/coq-num-analysisModuleSpace_compl:Merge branch 'master' of https://www-lipn.univ-paris13.fr/coq-num-analysis- Add and prove theta_cur_Def2_aux, minus_mult_div, sub_add_aux.Function_compl: