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.09Feb876432131Jan30282726252423201918171613109612Dec986130Nov28252322212017161514111094331Oct2827252120191817161312109876543229Sep2826222120191716141397652131Aug302310Jul874130Jun292827242322212017161514131098732130May25242320191817Linalg_compl:WIP: explore new path with comb_lin_l_{surj,inj,bij}Linalg_compl:Finite_family:Rename: span_ext -> span_eq.Proof of is_free_pairF_equiv.Don't name when unnecessary.Add 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.