sync master #14585
Merged
sync master #14585
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
For `a > 1`, `a ^ b = a` iff `b = 1`. Lemma needed by #14049. Co-authored-by: Ruben Van de Velde <[email protected]>
Co-authored-by: Riccardo Brasca <[email protected]>
This lemma doesn't mention any functors, so can go much earlier.
Mathlib's documentation generation CI uses a downstream repository, which just has a conventional `require` on both Mathlib and docgen. As far as I'm aware (please correct me!) this isn't actually needed by anyone. We are very keen to get rid of `meta if`, move to `lakefile.toml`s, and avoid instructing users to ever use `lake -R`. If this change works, I hope that the downstream mathematical repositories that are also using docgen can all follow suit.
The old naming is a remnant of Lean 3. The change has already been made for the Bochner integral, from `set_integral` to `setIntegral`.
* Forgot to incorporate 1 review comment from #14165
This PR has some basic lemmas for the `Ring.multichoose` function. They are generalizations of corresponding lemmas for `Nat.multichoose`.
The `unusedTactic` linter emits a warning if a tactic does nothing. Previous PRs (see below) removed all the "unused tactics" that the linter flagged. Here is an overview of this PR: * the linter is defined in `Mathlib/Tactic/Linter/UnusedTactic.lean`; * the file `Mathlib/GroupTheory/Perm/Cycle/Concrete.lean` contains the "only" `set_option` to opt out of the linter, since it defines notation that uses `decide` that the notation itself does not use; * 17 test files that have surgically opted out of the linter; * noise to import the new file, place it low in the import hierarchy and update `noshake`. PRs removing some unused tactics: * #11333 * #11351 * #11365 * #11379 [Zulip thread](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/pointless.20tactic.20linter)
…4277) add equiv_def and missing Trans instances to PGame
…or.map₂Iso` (#13900) This PR adds `OplaxFunctor.map₂Iso` and `Pseudofunctor.map₂Iso`, analogous to `Functor.mapIso`, and develops the corresponding API.
…le types (#14205) Namely: * `AList` * `Cycle` * `ConjAct` * `Projectivization` * `Lex` * `NatOrdinal` * `WithLawson` * `WithLower` * `WithUpper` * `WithScott` * `WithUpperSet` * `WithLowerSet` * `Speicalization` (which had an incorrectly-stated induction principle) These are just for the cases which have docstrings of the form "Use as `induction .* using .*`". Inspired by #12605.
These are no longer needed after #13264
Add some stacks tags to etale, flat, unramified etc morphisms. This contribution was created as part of the AIM workshop "Formalizing algebraic geometry" in June 2024.
#14289) Co-authored-by: Floris van Doorn <[email protected]>
This PR adds API for inverse and division of extended reals. Co-authored-by: @D-Thomine
Fix a missing edge case in the linter, when an option name had only one component (as in the profiler option), and add a test. At the same time, rewrite the linter to use the `name` API (much nicer!), and perform two small clean-ups to the test file.
And remove superfluous open's in Order/ExtendFrom.
For the same reason as the other existing options: these are not meant to stay in production code.
And delete one porting note which very surely seems non-actionable.
The remaining uses are - three declarations in Logic/Basic (which need it, somehow) - in UnivLE, where removing this yields funky errors related to explicit universe levels - in Logic/Equiv/Basic, which is a huge file; fixing it is less trivial
A more straightforward proof and we can reduce the explicit imports for `Data.NNRat.Defs` by a third.
… notes (#14552) Co-authored-by: Moritz Firsching <[email protected]>
Co-authored-by: Moritz Firsching <[email protected]>
Follow mathlib style slightly better: "Use spaces on both sides of ":", ":=" or infix operators." Automatically generated. Not exhaustive, as doing that everywhere has false positives with meta code.
We split `RingTheory.Trace` in `RingTheory.Trace.Defs` and `RingTheory.Trace.Basic`. Similarly for `RingTheory.Norm`.
Not exhaustive: hand-minimized in a few selected files
This PR makes the `set_option` linter only emit its warnings in files whose path begins with `Mathlib`, `test`, `Archive`, `Counterexamples`. Effectively, it should disable the linter on projects that are not mathlib. [Zulip thread](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/.60pp.2Emvars.60.20forbidden.3F/near/449962160)
…nd `Module` instance files (#14461) When we need algebra structures on `PUnit`, we should be more surgical about what we are importing. Co-authored-by: Matthew Robert Ballard <[email protected]>
Control/Random is left untouched for now; that file seems to use autoImplicits quite pervasively
This is not exhaustive: there are about ten remaining files in this directory. `Data/Vector` may come in a follow-up PR (this is harder).
Co-authored-by: Scott Morrison <[email protected]>
…#14536) We split off the results depending on `LinearOrderedSemifield` into a separate file. Co-authored-by: Michael Rothgang <[email protected]>
This PR allows to change the tactics that the unused tactic linter ignores. The main use-case is allowing `done` at the end of proofs, which is very useful for teaching purposes. See for instance [this Zulip thread](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Disable.20.60linter.2EunusedTactic.60.20warning.20for.20.60done.60).
These have no effect. Changes were automatically generated and then manually tweaked. Sometimes, fix indentation of subsequent lines instead of using semicolons.
We show Eisenstein series are modular forms. Co-authored-by: Chris Birkbeck <[email protected]>
…lCase (#14533) In some theorem names, `int_valuation` was still used instead of `intValuation`, and this PR fixes this.
Adds the insert version, golfs existing versions using `inferInstanceAs`. Makes the lemmas all consistent about using `Decidable` vs `DecidablePred`. These decidability instances are useful in downstream applications. Co-authored-by: Bhavik Mehta <[email protected]>
I am resigning as a maintainer
…lizations (#14163) This PR adds two missing theorems in `Mathlib.Data.Fintype.Basic`, which is in asisstant of the other PR of mine formalized some basic theorems in `GameTheory.AuctionTheory.Basic` . One may check the previous PR for Auction Theory here: #13248 I would sincerely appreciate a timely review of this PR, as I am eager to complete my first project on Auction Theory before my upcoming birthday. Thank you very much for your consideration and support! Co-authored-by: Wang Haocheng <[email protected]>
…#14328) Adds a `MorphismProperty.stalkwise` constructor for morphism properties of schemes from a property of ring homomorphisms. Also adds API for reducing proofs of stability under base change to affine situations for properties local at the target.
#14528) Let `C` be a pretriangulated category. In this PR, we show that the functors `preadditiveCoyoneda.obj A : C ⥤ AddCommGrp` for `A : Cᵒᵖ` and `preadditiveYoneda.obj B : Cᵒᵖ ⥤ AddCommGrp` for `B : C` are homological functors.
Accidentally created a `Mathlib/NumberTheory/ModularForms/EisensteinSeries/ModularForm.lean` file name. Made it a Basic.lean file and made the previous into a Defs.lean
This only changes incremental compilation.
The now redundant old homology API is removed. (It was already mostly unused.) The only slightly non-trivial changes are in `CategoryTheory.Abelian.Exact` where some definitions and proofs have been refactored. The proof that the category of abelian groups satisfies Grothendieck's AB5 axiom had to be moved to a separate file `Algebra.Category.Grp.AB5`.
Put congruence subgroups into their own namespace, so that things like `Gamma` don't live in the root namespace.
This PR updates the Mathlib dependencies.
PR summary a42993dbc5
|
| Files | Import difference |
|---|---|
Mathlib.Topology.MetricSpace.PartitionOfUnity Mathlib.Analysis.Convex.PartitionOfUnity |
43 |
Mathlib.Topology.Category.Profinite.Nobeling |
65 |
3 filesMathlib.Condensed.Light.Explicit Mathlib.Condensed.Light.TopComparison Mathlib.Condensed.Light.Module |
80 |
5 filesMathlib.Condensed.Limits Mathlib.Condensed.TopComparison Mathlib.Condensed.Explicit Mathlib.Condensed.Module Mathlib.Condensed.Solid |
81 |
Mathlib.Topology.PartitionOfUnity |
82 |
8 filesMathlib.Topology.Category.LightProfinite.EffectiveEpi Mathlib.Topology.CompletelyRegular Mathlib.Topology.Category.LightProfinite.Limits Mathlib.Topology.Category.LightProfinite.Basic Mathlib.Condensed.Light.Basic Mathlib.Condensed.Light.Discrete Mathlib.Condensed.Light.Functors Mathlib.MeasureTheory.Measure.EverywherePos |
92 |
23 filesMathlib.Topology.Category.Stonean.Adjunctions Mathlib.Topology.Category.Stonean.EffectiveEpi Mathlib.Topology.Category.CompHaus.EffectiveEpi Mathlib.Topology.Category.Profinite.CofilteredLimit Mathlib.Topology.Category.Profinite.EffectiveEpi Mathlib.Topology.Category.Profinite.AsLimit Mathlib.Condensed.Basic Mathlib.Topology.Category.CompHaus.Basic Mathlib.Topology.Category.CompHaus.Projective Mathlib.Topology.Category.Profinite.Projective Mathlib.Topology.Category.Profinite.Basic Mathlib.Topology.Category.CompHaus.Limits Mathlib.Topology.Category.Compactum Mathlib.Topology.Category.Stonean.Basic Mathlib.Topology.Category.Locale Mathlib.Order.Category.Frm Mathlib.Condensed.Discrete Mathlib.Condensed.Functors Mathlib.Condensed.Equivalence Mathlib.Topology.Category.Profinite.Product Mathlib.Topology.Category.Profinite.Limits Mathlib.Topology.Order.Category.FrameAdjunction Mathlib.Topology.Category.Stonean.Limits |
93 |
Mathlib.Topology.UrysohnsLemma |
94 |
Declarations diff
+ exists_forall_tsupport_iUnion_one_iUnion_of_isOpen_isClosed
+ exists_tsupport_one_of_isOpen_isClosed
You can run this locally as follows
## summary with just the declaration names:
./scripts/no_lost_declarations.sh short <optional_commit>
## more verbose report:
./scripts/no_lost_declarations.sh <optional_commit>
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.
No description provided.