mathlib3
feat(analysis/normed_space/lp_space): "functoriality" of `lp`
#15754
Open
Overview
Commits
18
Changes
View On GitHub

feat(analysis/normed_space/lp_space): "functoriality" of `lp` #15754

ADedecker wants to merge 18 commits into master from AD_lp_functorial
ADedecker
ADedecker Start
e7938ed6
ADedecker ...
89a9ab9e
ADedecker Useless
28290053
ADedecker Basics
2db919b2
ADedecker Congr right
266ab572
ADedecker ADedecker added WIP
ADedecker Fixes
738aed0c
ADedecker ADedecker removed WIP
ADedecker ADedecker added awaiting-review
ADedecker ADedecker removed awaiting-review
ADedecker ADedecker added WIP
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
vihdzp
vihdzp commented on 2022-07-30
ADedecker Update src/analysis/normed_space/lp_space.lean
4c25aeb0
ADedecker Finish renaming
9ff6e5a4
ADedecker Semilinearize
4f4f6209
ADedecker ADedecker removed WIP
ADedecker ADedecker added awaiting-review
ADedecker ADedecker added t-analysis
ADedecker Better definition of `congr_right`
f28c79e5
PatrickMassot PatrickMassot assigned hrmacbeth hrmacbeth 3 years ago
mcdoll
mcdoll
mcdoll commented on 2022-10-02
j-loreaux j-loreaux removed awaiting-review
j-loreaux j-loreaux added awaiting-author
eric-wieser Update src/analysis/normed_space/lp_space.lean
418f202b
eric-wieser style fixes
c1dc62c9
eric-wieser Merge remote-tracking branch 'origin/master' into AD_lp_functorial
5cf02734
eric-wieser
eric-wieser commented on 2023-03-16
eric-wieser eric-wieser added awaiting-CI
eric-wieser fix norm notation
e06c9d1d
eric-wieser move types to variables lines
a828fefb
github-actions github-actions removed awaiting-CI
eric-wieser
kim-em kim-em added too-late

Login to write a write a comment.

Login via GitHub

Reviewers
Assignees
Labels
awaiting-author t-analysis too-late
Milestone
No milestone
Terms Of Use Privacy Policy Refund Policy Impressum