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
9931a69d8182b49b8ec002072bfddffc93b0c176
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
1
Feb
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
16
14
13
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
Propagate notations for plus, opp and minus, and definition ones.
Add notations for opp and minus, definition of ones (no need for zeros),
WIP comb_lin
Move a section
comb_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 kronecker
Merge branch 'master' of https://depot.lipn.univ-paris13.fr/mayero/coq-num-analysis
WIP comb_lin
Fix 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_concatF
Add 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-analysis
Work on Lagrange section.
Not anymore! ;)
Proofs of concatF_nil_{l,r} and concatF_last.
Remove injF, since it was an instance of injective...
Loading