mathlib3
feat(analysis/normed_space/lp_space): currying for `lp` spaces
#15781
Open
Overview
Commits
17
Changes
View On GitHub

feat(analysis/normed_space/lp_space): currying for `lp` spaces #15781

ADedecker wants to merge 17 commits into master from AD_lp_curry
ADedecker
ADedecker Start
e7938ed6
ADedecker ...
89a9ab9e
ADedecker Useless
28290053
ADedecker Basics
2db919b2
ADedecker Congr right
266ab572
ADedecker Fixes
738aed0c
ADedecker ++
53e99595
ADedecker Name clash
8fab2bd5
ADedecker Make `function.injective.decidable_eq` protected
9af03251
ADedecker Merge branch 'AD_injective_decidable_eq_protected' into AD_lp_functorial
c7f9f618
ADedecker Update src/analysis/normed_space/lp_space.lean
4c25aeb0
ADedecker Finish renaming
9ff6e5a4
ADedecker Semilinearize
4f4f6209
ADedecker Merge branch 'AD_lp_functorial' into AD_lp_curry
f9e84f27
ADedecker Done
11bbcb9d
ADedecker ADedecker added awaiting-review
ADedecker ADedecker added t-analysis
ghost ghost added blocked-by-other-PR
ghost
ADedecker Better definition of `congr_right`
f28c79e5
ADedecker Merge branch 'AD_lp_functorial' into AD_lp_curry
c9cbcff7
eric-wieser eric-wieser added not-too-late
ADedecker
ADedecker ADedecker removed not-too-late
ADedecker ADedecker added too-late

Login to write a write a comment.

Login via GitHub

Reviewers
No reviews
Assignees
No one assigned
Labels
awaiting-review blocked-by-other-PR t-analysis too-late
Milestone
No milestone
Terms Of Use Privacy Policy Refund Policy Impressum