lp_space): "functoriality" of `lp`
#15754

Open

Commits

Start

ADedecker committed 3 years ago
...

ADedecker committed 3 years ago
Useless

ADedecker committed 3 years ago
Basics

ADedecker committed 3 years ago
Congr right

ADedecker committed 3 years ago
Fixes

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
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
Better definition of `congr_right`

ADedecker committed 3 years ago
Update src/analysis/normed_space/lp_space.lean

eric-wieser committed 2 years ago
style fixes

eric-wieser committed 2 years ago
Merge remote-tracking branch 'origin/master' into AD_lp_functorial

eric-wieser committed 2 years ago
fix norm notation

eric-wieser committed 2 years ago
move types to variables lines

eric-wieser committed 2 years ago