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.08Feb76432131Jan30282726252423201918171613109612Dec986130Nov28252322212017161514111094331Oct2827252120191817161312109876543229Sep2826222120191716141397652131Aug302310Jul874130Jun292827242322212017161514131098732130May25242320191817Add plus_is_zero.Add lt_2_dec and prove ord2_dec.Oups, wrong!Skip unused.Optim Imports.Optim Imports.Optim Imports.Optim Imports.Add some doc.Propagate renaming.Optim Imports.Use new eqF.Optim Imports.Optim Imports.Optim Imports.Add singlF_0, pairF_0 and pairF_1.Add minus_zero_l and minus_zero_r.Add and prove results on singlF/pairF:Réunion 6/02/231 lemme trivialCleanNettoyage Canonical + preuves dual_basis2 (avec vsub)Nettoyage en-têtesEt merge !!WIP: is_free_singlF_equiv.Add and prove in_I_1 and in_I_2.Add and prove is_generator_nil, is_basis_nil and has_dim_0.Extract complements on linear algebra (module spaces and linear mappings),Merge branch 'master' of depot.lipn.univ-paris13.fr:mayero/coq-num-analysisAdd and prove span_nil, is_free_nil and is_free_not_zero.Preuve comb_lin_inclF_inj !Patch proofs (for new def of is_generator).Reorder and rename lemmas on span.preuve de comb_lin_inclF (un peu long et douloureux...)Add and prove (missing) basic lemmas on groups.Def 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-analysis