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.01Feb31Jan30282726252423201918171613109612Dec986130Nov28252322212017161514111094331Oct2827252120191817161312109876543229Sep2826222120191716141397652131Aug302310Jul874130Jun292827242322212017161514131098732130May25242320191817161413Def zero_struct.ker is there, but bof!Proofs of compatibility of is_linear_mapping with image and preimage.Compatibility of morphism_g with image and preimage.Merge branch 'master' of depot.lipn.univ-paris13.fr:mayero/coq-num-analysisPropagate notations for plus, opp and minus, and definition ones.Add notations for opp and minus, definition of ones (no need for zeros),WIP comb_linMove a sectioncomb_lin++Add and prove span_glb (with comb_lin_ind).Add comb_lin_ind (to be proved).Add and prove span_inF.Add and prove inF_monot, concatF_lub, concatF_inclF_{l,r}.Factor context.Add and prove span_inF_fun.Add and prove span_concatF_sym_inF.WIP comb_lin et simplification kroneckerMerge branch 'master' of https://depot.lipn.univ-paris13.fr/mayero/coq-num-analysisWIP comb_linFix the hint for comb_lin_inclF.Apparently it is OK now (at least here).WIP span_concatF_compat_r: use same proof path as span_concatF_compat_l.Add comb_lin_one and comb_lin_two (wip).Add is_free_is_injective (wip).Rename: comb_lin_one -> comb_lin_singl.Add ex_neq_not_eqF.concatF_last: addnS does the job!preuve comb_lin_concatFAdd lemmas about span (span_incl, span_ext, span_concatF_sym, span_{scal,plus}_compat).WIP: concatF_split.Use inclF.Add and prove castF_refl.Add definition inF and lemmas castF_eq_sym_{l,r}.Move is_linear_mapping_f_scal_l at the beginning.Merge branch 'master' of https://www-lipn.univ-paris13.fr/coq-num-analysisWork on Lagrange section.Not anymore! ;)Proofs of concatF_nil_{l,r} and concatF_last.Remove injF, since it was an instance of injective...