[Merged by Bors] - feat(analysis/*): a sample of easy useful lemmas #13697
Conversation
sgouezel
added
the
awaiting-review
| @@ -105,6 +105,9 @@ by simpa using cpow_neg x 1 | |||
| complex.zero_cpow (nat.cast_ne_zero.2 (nat.succ_ne_zero _)), zero_mul] | |||
| else by simp [cpow_add, hx, pow_add, cpow_nat_cast n] | |||
|
|
|||
| @[simp] lemma cpow_two (x : ℂ) : x ^ (2 : ℂ) = x ^ 2 := | |||
There was a problem hiding this comment.
Should these be tagged norm_cast?
There was a problem hiding this comment.
There is no cast here (the 2 on the left is not the coercion from nat to complex, it is just the complex 2), so norm_cast does not work. On the other hand, there was a missing norm_cast attribute on nearby lemmas!
src/analysis/normed/group/basic.lean
Outdated
| @@ -1020,6 +1020,14 @@ begin | |||
| exact (tendsto_at_top_of_eventually_const this).cauchy_seq.add hv | |||
| end | |||
|
|
|||
| lemma normed_group.tendsto_sub_nhds_zero_iff | |||
There was a problem hiding this comment.
Can this be closer to squeeze_zero_norm and other filter-norm lemmas?
There was a problem hiding this comment.
No, because the proof uses the topological group instance which is proved just a few lines above.
src/analysis/normed/group/basic.lean
Outdated
| @@ -1020,6 +1020,14 @@ begin | |||
| exact (tendsto_at_top_of_eventually_const this).cauchy_seq.add hv | |||
| end | |||
|
|
|||
| lemma tendsto_sub_nhds_zero_iff | |||
There was a problem hiding this comment.
Shouldn't we prove this for any topological group (multiplicative or additive) rather than just normed?
|
✌️ sgouezel can now approve this pull request. To approve and merge a pull request, simply reply with |
leanprover-community-bot-assistant
added
delegated
|
bors r+ |
github-actions
bot
added
the
ready-to-merge
|
Pull request successfully merged into master. Build succeeded: |
bors
bot
changed the title
Lemmas needed for #13690