Better definition of `congr_right` - SemanticDiff

Commit

3 years ago

Better definition of `congr_right`

References

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

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

Author

ADedecker

ADedecker

Parents

Loading