Mitchell Lee

I would like to give `B →₀ ℝ` the instances `AddCommMonoid`, `OrderedCancelAddCommMonoid`, and `SMulPosMono` for this file only. I don't want to make the instances global. However, I do use...

Thanks for the feedback. I have made the changes you suggest.

I wonder whether these theorems should all be a special case of more general theorems for `Antiperiodic` functions (https://leanprover-community.github.io/mathlib4_docs/Mathlib/Algebra/Periodic.html#Function.Antiperiodic).

Hello, I've redone this branch so that it deduces the facts about sin and cos from more general facts about Antiperiodic functions.

> Why state half of your lemmas using `negOnePow` and the other half using `(-1)^n`? You can't write simply `(-1) ^ n` if `n` is an integer, only if it's...

Good point. Does that mean I should state the lemmas about trigonometric functions using `(-1) ^ n`, but continue to use `negOnePow` for the general lemmas about antiperiodic functions?

After playing around with this, I now think that `Field.zpow` is so difficult to work with that it would be better to leave it as `negOnePow` for now. Unless I...

ok, I've fixed it. thanks!

One question I have for the reviewers is what folder this file should be in (`Mathlib.Topology.Algebra.InfiniteSum.Nonarchimedean`, or `Mathlib.Topology.Algebra.Nonarchimedean.InfiniteSum`?) . The other is what namespace the theorems should be in (`NonarchimedeanAddGroup.summable_iff_tendsto_cofinite_zero`,...

I made this proof more complicated than it needs to be. I can simplify it by using `cauchySeq_finset_iff_vanishing`. I will work on this.