Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

refactor(analysis/normed_space/basic) Remove outparam in normed space #844

Merged
merged 1 commit into from
Mar 27, 2019

Conversation

sgouezel
Copy link
Collaborator

There are still outparams in the definition of normed_space, probably forgotten in the module refactor. A consequence is that is_bounded_linear_maps and has_fderiv have been defined without mentioning explicitely the field of scalars. This makes it impossible to distinguish R-bounded linear maps and C-bounded linear maps on a complex vector space, or to distinguish between the real derivative and the complex derivative.

We remove the outparam in the definition, and add the field of scalars where necessary.

This PR conflicts with virtually all my recent PRs, I guess, but I think this one should be merged first (and if possible rapidly, otherwise conflicts will show up again quickly) and then I will rebase the other PRs.

Copy link
Member

@jcommelin jcommelin left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

As far as I can see this is very straightforward and in line with the current trend with modules. Let's get this merged.

@avigad
Copy link
Collaborator

avigad commented Mar 27, 2019

@jcommelin Thanks, this is helpful. It looks good to me, so I'll merge.

@avigad avigad merged commit 02ca494 into leanprover-community:master Mar 27, 2019
@sgouezel sgouezel deleted the remove_outparam branch December 2, 2019 10:38
anrddh pushed a commit to anrddh/mathlib that referenced this pull request May 15, 2020
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

None yet

3 participants