[Merged by Bors] - feat: scalar tower instances for quotients #22951
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
PR summary 8e33c76fbeImport changes for modified filesNo significant changes to the import graph Import changes for all files
|
|
Thanks! bors merge |
leanprover-community-mathlib4-bot
added
the
ready-to-merge
mathlib-bors bot
pushed a commit
that referenced
this pull request
Mar 15, 2025
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`.
|
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.
We already have the
SMulCommClassandIsScalarTowerversions forRingQuot; this develops them forConandRingCon, with the eventual aim of replacingRingQuotwithRingCon.Quotient.