mathlib3
feat(analysis/inner_product_space/l2_space.lean): collect Hilbert bases along a Hilbert sum decomposition
#15791
Open
Open
feat(analysis/inner_product_space/l2_space.lean): collect Hilbert bases along a Hilbert sum decomposition #15791
ADedecker
wants to merge
38 commits into
master
from
AD_subordinate_hilbert_basis
Dependent type hell
2fd5e111
++
100196fa
I should think
14169dc7
Success !
c5bcbff8
Clean
80f9026d
Main thm !
24f5ad1c
Small progress
9b95fdf9
DTT hell strikes again
9dca747e
Induction is incredible
e7a0d977
Super annoying timeout
3bd3af67
Timeout fixed :tada:
4e73262c
Indentation
10231e42
Done ?
66df8034
Start
e7938ed6
...
89a9ab9e
Useless
28290053
Basics
2db919b2
Congr right
266ab572
Fixes
738aed0c
++
53e99595
Use `expand_exists`
d75d48ff
Name clash
8fab2bd5
Make `function.injective.decidable_eq` protected
9af03251
Merge branch 'AD_injective_decidable_eq_protected' into AD_lp_functorial
c7f9f618
Define`is_hilbert_sum` predicate
691c6557
Update src/analysis/normed_space/lp_space.lean
4c25aeb0
Finish renaming
9ff6e5a4
Semilinearize
4f4f6209
Lint
30df7ef0
Merge branch 'AD_lp_functorial' into AD_lp_curry
f9e84f27
Done
11bbcb9d
Merge branch 'AD_lp_curry' into AD_subordinate_hilbert_basis
e4be6302
Merge remote-tracking branch 'origin/AD_is_hilbert_sum' into AD_subor…
875443fd
Collect Hilbert bases along a Hilbert sum decomposition
21ef33c8
Long line
19c3fab9
Unused arguments
3ad9537f
Stray `#lint`
ea019458
Merge remote-tracking branch 'origin/master' into AD_subordinate_hilb…
abdd94e9
Reviewers
No reviews
Assignees
No one assigned
Labels
awaiting-review
blocked-by-other-PR
t-analysis
too-late
Milestone
No milestone
Login to write a write a comment.
Login via GitHub