[Merged by Bors] - feat(Data/Complex/Trigonometric): closer upper bound for cos 1 #22945
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
cos 1 is approximately 0.5403..., so this bound is fairly tight.
github-actions
bot
added
the
new-contributor
PR summary 1b4b7b8380Import changes for modified filesNo significant changes to the import graph Import changes for all files
Declarations diffNo declarations were harmed in the making of this PR! 🐙 You can run this locally as follows## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>
## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>The doc-module for No changes to technical debt.You can run this locally as
|
vlad902
added
the
easy
jhanschoo
changed the title
jhanschoo
changed the title
|
I changed the title of the PR: "tight" is jargon for exact (in certain instances), so the present title (which will become the commit message) was misleading. |
grunweg
changed the title
|
🚀 Pull request has been placed on the maintainer queue by grunweg. |
|
Thanks! bors merge |
leanprover-community-mathlib4-bot
added
ready-to-merge
mathlib-bors bot
pushed a commit
that referenced
this pull request
Mar 16, 2025
cos 1 is approximately 0.5403..., so this bound is fairly tight. Co-authored-by: Vlad Tsyrklevich <[email protected]>
|
Pull request successfully merged into master. Build succeeded: |
mathlib-bors
bot
changed the title
qawbecrdtey
added a commit
that referenced
this pull request
Mar 17, 2025
…vProdLpPiLp` (#22993) * feat: scalar tower instances for quotients (#22951) We already have the `SMulCommClass` and `IsScalarTower` versions for `RingQuot`; this develops them for `Con` and `RingCon`, with the eventual aim of replacing `RingQuot` with `RingCon.Quotient`. * chore(Order/Group/Abs): use `@[to_additive]` (#22468) * feat(FieldTheory/Finite/Basic): lemmas about the prime subfield in positive characteristic (#22843) This PR adds some elementary results about the prime subfield of a characteristic p field, e.g., size is p, elements are integer multiples of one, and elements are characterized by being fixed by the p-th power map. * docs(Data/Real/EReal): fix capitalization error (#22943) Changes `Ereal` to `EReal` in the module docstring for `Data/Real/EReal`. * chore(Ideal/Quotient): change `Fintype` to `Finite` (#22947) As discussed [here](#22902 (comment)) * feat: add `norm_num` extensions for factorials (#8832) Add `norm_num` extensions to evaluate `Nat.factorial`, `Nat.ascFactorial` and `Nat.descFactorial`. Co-authored-by: Eric Wieser <[email protected]> * perf(CategoryTheory/Limits/Shapes): reorder instance arguments (#22968) This PR is in the same spirit as #22953. The problem is that some instances about category theoretical limits have silly side conditions that end up searching through the whole algebraic type class hierarchy. This PR attempts to keep the type class search limited to category theoretical type classes. * feat(LinearAlgebra/FreeModule/CardQuotient): compute indices of subgroups via determinant (#22940) * feat: API for continuous extension of meromorphic functions (#22867) Defines the normal form of meromorphic functions and provides API for continuous extension, as discussed [on Zulip](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/API.20for.20continuous.20extension.20of.20meromorphic.20functions). More material will be provided in upcoming PRs. This material is used in [Project VD](https://github.com/kebekus/ProjectVD), which aims to formalize Value Distribution Theory for meromorphic functions on the complex plane. * feat(Data/Complex/Trigonometric): closer upper bound for cos 1 (#22945) cos 1 is approximately 0.5403..., so this bound is fairly tight. Co-authored-by: Vlad Tsyrklevich <[email protected]> * chore: move `List.Lex` lemmas out of the `List.Lex` namespace (#22935) This better matches the naming convention. * working on it. * Added sup_disjSum and inf_disjSum. * Finished one branch. * Finished proof. --------- Co-authored-by: Eric Wieser <[email protected]> Co-authored-by: Yury G. Kudryashov <[email protected]> Co-authored-by: Scott Carnahan <[email protected]> Co-authored-by: plp127 <[email protected]> Co-authored-by: Xavier Roblot <[email protected]> Co-authored-by: Sebastian Zimmer <[email protected]> Co-authored-by: JovanGerb <[email protected]> Co-authored-by: Stefan Kebekus <[email protected]> Co-authored-by: Vlad Tsyrklevich <[email protected]> Co-authored-by: Vlad Tsyrklevich <[email protected]> Co-authored-by: Yaël Dillies <[email protected]>
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
cos 1 is approximately 0.5403..., so this bound is fairly tight.