Skip to content
GitLab
Explore
Sign in
Primary navigation
Search or go to…
Project
N
Numerical Analysis in Coq
Manage
Activity
Members
Labels
Plan
Issues
Issue boards
Milestones
Wiki
Code
Merge requests
Repository
Branches
Commits
Tags
Repository graph
Compare revisions
Snippets
Build
Pipelines
Jobs
Pipeline schedules
Artifacts
Deploy
Releases
Package Registry
Model registry
Operate
Environments
Terraform modules
Monitor
Incidents
Analyze
Value stream analytics
Contributor analytics
CI/CD analytics
Repository analytics
Model experiments
Help
Help
Support
GitLab documentation
Compare GitLab plans
Community forum
Contribute to GitLab
Provide feedback
Keyboard shortcuts
?
Snippets
Groups
Projects
Show more breadcrumbs
Micaela Mayero
Numerical Analysis in Coq
Graph
336b65b7b8bfb7a6458224a51c03249ff5d72539
Select Git revision
Branches
7
Subset
essais-8.18
master
default
protected
no_ms
pr_no_math-comp
released
test_skolem_ko
Tags
5
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.
Begin with the selected commit
Created with Raphaël 2.2.0
8
Feb
7
6
4
3
2
1
31
Jan
30
28
27
26
25
24
23
20
19
18
17
16
13
10
9
6
12
Dec
9
8
6
1
30
Nov
28
25
23
22
21
20
17
16
15
14
11
10
9
4
3
31
Oct
28
27
25
21
20
19
18
17
16
13
12
10
9
8
7
6
5
4
3
2
29
Sep
28
26
22
21
20
19
17
16
14
13
9
7
6
5
2
1
31
Aug
30
23
10
Jul
8
7
4
1
30
Jun
29
28
27
24
23
22
21
20
17
16
15
14
13
10
9
8
7
3
2
1
30
May
25
24
23
20
19
18
17
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/23
1 lemme trivial
Clean
Nettoyage Canonical + preuves dual_basis2 (avec vsub)
Nettoyage en-têtes
Et 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-analysis
Add 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
Loading