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
[Merged by Bors] - chore(analysis/normed_space): define norm_one_class
#4323
Conversation
Many normed rings have `∥1⊫1`. Add a typeclass mixin for this property.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
This all looks good to me. @PatrickMassot any thoughts?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Normed algebras (according to the current definition) will satisfy norm_one_class
, right? Could you add this instance?
This can't be an instance because Lean can't guess |
LGTM. Since @PatrickMassot was pinged earlier, let's leave it open til he wakes up. |
bors merge |
Many normed rings have `∥1⊫1`. Add a typeclass mixin for this property. API changes: * drop `normed_field.norm_one`, use `norm_one` instead; * same with `normed_field.nnnorm_one`; * new typeclass `norm_one_class` for `∥1∥ = 1`; * add `list.norm_prod_le`, `list.norm_prod_le`, `finset.norm_prod_le`, `finset.norm_prod_le'`: norm of the product of finitely many elements is less than or equal to the product of their norms; versions with prime assume that a `list` or a `finset` is nonempty, while the other versions assume `[norm_one_class]`; * rename `norm_pow_le` to `norm_pow_le'`, new `norm_pow_le` assumes `[norm_one_class]` instead of `0 < n`; * add a few supporting lemmas about `list`s and `finset`s.
Pull request successfully merged into master. Build succeeded: |
norm_one_class
norm_one_class
Many normed rings have `∥1⊫1`. Add a typeclass mixin for this property. API changes: * drop `normed_field.norm_one`, use `norm_one` instead; * same with `normed_field.nnnorm_one`; * new typeclass `norm_one_class` for `∥1∥ = 1`; * add `list.norm_prod_le`, `list.norm_prod_le`, `finset.norm_prod_le`, `finset.norm_prod_le'`: norm of the product of finitely many elements is less than or equal to the product of their norms; versions with prime assume that a `list` or a `finset` is nonempty, while the other versions assume `[norm_one_class]`; * rename `norm_pow_le` to `norm_pow_le'`, new `norm_pow_le` assumes `[norm_one_class]` instead of `0 < n`; * add a few supporting lemmas about `list`s and `finset`s.
Many normed rings have
∥1⊫1
. Add a typeclass mixin for this property.API changes:
normed_field.norm_one
, usenorm_one
instead;normed_field.nnnorm_one
;norm_one_class
for∥1∥ = 1
;list.norm_prod_le
,list.norm_prod_le
,finset.norm_prod_le
,finset.norm_prod_le'
:norm of the product of finitely many elements is less than or equal to the product of their norms;
versions with prime assume that a
list
or afinset
is nonempty, while the other versionsassume
[norm_one_class]
;norm_pow_le
tonorm_pow_le'
, newnorm_pow_le
assumes[norm_one_class]
insteadof
0 < n
;list
s andfinset
s.