mathlib3
feat(analysis/inner_product_space/l2_space.lean): collect Hilbert bases along a Hilbert sum decomposition
#15791
Open
Overview
Commits
38
Changes
View On GitHub
Commits
  • Dependent type hell
    ADedecker committed 4 years ago
  • ++
    ADedecker committed 4 years ago
  • I should think
    ADedecker committed 4 years ago
  • Success !
    ADedecker committed 4 years ago
  • Clean
    ADedecker committed 4 years ago
  • Main thm !
    ADedecker committed 4 years ago
  • Small progress
    ADedecker committed 4 years ago
  • DTT hell strikes again
    ADedecker committed 4 years ago
  • Induction is incredible
    ADedecker committed 4 years ago
  • Super annoying timeout
    ADedecker committed 4 years ago
  • Timeout fixed :tada:
    ADedecker committed 4 years ago
  • Indentation
    ADedecker committed 4 years ago
  • Done ?
    ADedecker committed 4 years ago
  • Start
    ADedecker committed 4 years ago
  • ...
    ADedecker committed 4 years ago
  • Useless
    ADedecker committed 4 years ago
  • Basics
    ADedecker committed 4 years ago
  • Congr right
    ADedecker committed 3 years ago
  • Fixes
    ADedecker committed 3 years ago
  • ++
    ADedecker committed 3 years ago
  • Use `expand_exists`
    ADedecker committed 3 years ago
  • Name clash
    ADedecker committed 3 years ago
  • Make `function.injective.decidable_eq` protected
    ADedecker committed 3 years ago
  • Merge branch 'AD_injective_decidable_eq_protected' into AD_lp_functorial
    ADedecker committed 3 years ago
  • Define`is_hilbert_sum` predicate
    ADedecker committed 3 years ago
  • Update src/analysis/normed_space/lp_space.lean
    ADedecker committed 3 years ago
  • Finish renaming
    ADedecker committed 3 years ago
  • Semilinearize
    ADedecker committed 3 years ago
  • Lint
    ADedecker committed 3 years ago
  • Merge branch 'AD_lp_functorial' into AD_lp_curry
    ADedecker committed 3 years ago
  • Done
    ADedecker committed 3 years ago
  • Merge branch 'AD_lp_curry' into AD_subordinate_hilbert_basis
    ADedecker committed 3 years ago
  • Merge remote-tracking branch 'origin/AD_is_hilbert_sum' into AD_subordinate_hilbert_basis
    ADedecker committed 3 years ago
  • Collect Hilbert bases along a Hilbert sum decomposition
    ADedecker committed 3 years ago
  • Long line
    ADedecker committed 3 years ago
  • Unused arguments
    ADedecker committed 3 years ago
  • Stray `#lint`
    ADedecker committed 3 years ago
  • Merge remote-tracking branch 'origin/master' into AD_subordinate_hilbert_basis
    ADedecker committed 3 years ago
FAQ Terms Privacy Refunds Impressum
Loading