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.024Jan23201918171613109612Dec986130Nov28252322212017161514111094331Oct2827252120191817161312109876543229Sep2826222120191716141397652131Aug302310Jul874130Jun292827242322212017161514131098732130May252423201918171614131211109WIP: proof of comb_lin_concatF.Add concatF_last (admitted).Move stuff to Finite_family (new) and comb_lin.Move notation 'E^n to Finite_family.Collect in new file Finite_family all stuff on 'E^n with no structure on E.New def for castF.passage dans poly_Lagrangessr_Coquelicot and Coquelicot_ssr are no longer used.ssr_Coquelicot and Coquelicot_ssr are no longer used.QUIET!Oups, now using SSReflect: have to force standard "rewrite" with "->".Move stuff around.Apparently, both conclusions of Steinitz exchange lemma are proved together·Borrow concat from sandbox (renamed concatF).ex_span -> span_ex.Highlight lemmas that are already explicitly used.Pas d'admits dans comb_linsimplify the proof of FE_is_unisolvant_cur lemma.Hint: @Sg E PE...Use magic: subst!Reorganize.Tune imports.Merge branch 'master' of depot.lipn.univ-paris13.fr:mayero/coq-num-analysisReorder + proof of compose_is_surj_compat, is_surj_compose andEssais SBReorganize + proof of compose_is_inj_compat and is_inj_compose (statement modified).Proof of compose_range_compat, compose_identity_compat, and compose_is_bij_id_compat.Reorder + proof of compose_is_bij_compat.Reorder + proof of is_bij_equiv.New section + proof of comb_lin_kronecker_product.Reorder + proof of comb_lin_scal_l (to be renamed).compose needs 3 sets -> new section.Merge branch 'master' of depot.lipn.univ-paris13.fr:mayero/coq-num-analysisWIP: comb_lin_ext_gen.Finish the proof of FE_is_unisolvant_cur lemma.Proof of FE_is_unisolvant_cur (WIP)remove is_linear_mapping_sigma_cur_aux lemma (not necessary).move and prove cur_to_ref_bij lemma.Add cur_to_ref_bij (admitted).Reorganization (= move stuff).