This repository has been archived by the owner on Jul 24, 2024. It is now read-only.
Make prime-avoidance branch build #4925
Merged
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
Another condition equivalent to the sheaf condition: for every open cover `U`, `F.obj (supr U)` is the limit point of the diagram consisting of all the `F.obj V`, where `V ≤ U i` for some `i`. This condition is particularly straightforward to state, and makes some proofs easier (however we don't do this here: just prove the equivalence with the "official" definition). It's particularly nice because there is no case splitting (depending on whether you're looking at single or double intersections) when checking the sheaf condition. This is the statement Lurie uses in Spectral Algebraic Geometry. Later I may propose that we make this the official definition, but I'll wait to see how it pans out in actual use, first. For now it's just provided as yet another equivalent version of the sheaf condition. Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Continuation of a discussion at #4518
…hat it is multiplicative (#4393) Defines `polynomial.content` to be the `gcd` of the coefficients of a polynomial Says a polynomial `is_primitive` if its content is 1 Proves that `(p * q).content = p.content * q.content
…n f is injective (#4645) This puts much weaker restrictions on `h`, making this easier to apply in some situations
…rmalization_monoid` on polynomials (#4655) Defines a `normalization_monoid` instance on any `comm_group_with_zero`, including fields Defines a `normalization_monoid` instance on `polynomial R` when `R` has a `normalization_monoid` instance Co-authored-by: Johan Commelin <johan@commelin.net>
* `prod.left_cancel_semigroup`; * `prod_right_cancel_semigroup`; * `prod.ordered_cancel_comm_monoid`; * `ordered_comm_group`.
…ne_subspace` (#4643) * now `line_map` takes two points on the line, not a point and a direction, update/review lemmas; * add `submodule.to_affine_subspace`; * add `affine_map.fst` and `affine_map.snd`; * prove that an affine map `ℝ → ℝ` sends an unordered interval to an unordered interval.
…leanup (#4656) Renames: - `discriminant_le_zero` to `discrim_le_zero` - `discriminant_lt_zero` to `discrim_lt_zero`
…ure (#4639) This definition is useful for proving the Lebesgue-Radon-Nikodym theorem for non-negative measures. Co-authored-by: mzinkevi <41597957+mzinkevi@users.noreply.github.com>
…4519) Previously `solve_by_elim*` would operate on multiple goals (only succeeding if it could close all of them, and performing backtracking across goals), however it would incorrectly only use the local context from the main goal. If other goals had different sets of hypotheses, ... various bad things could happen! This PR arranges so that `solve_by_elim*` inspects the local context later, so it picks up the correct hypotheses. Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
The goal is to make `nontriviality` work for the following goals: * [x] `nontriviality α` if the goal is `is_open s`, `s : set α`; * [x] `nontriviality E` if the goal is `is_O f g` or `is_o f g`, where `f : α → E`; * [x] `nontriviality R` if the goal is `linear_independent R _`; * [ ] `nontriviality R` if the goal is `is_O f g` or `is_o f g`, where `f : α → E`, `[semimodule R E]`; in this case `nontriviality` should add a local instance `semimodule.subsingleton R`. The last case was never needed in `mathlib`, and there is a workaround: run `nontriviality E`, then deduce `nontrivial R` from `nontrivial E`. Misc feature: * [x] make `nontriviality` accept an optional list of additional `simp` lemmas. Co-authored-by: Rob Lewis <rob.y.lewis@gmail.com>
Use `M`, `N`, `P` for types with `has_zero`, `add_monoid`, or `add_comm_monoid` structure, and `R`, `S` for types with at least a `semiring` instance. API change: `single_add_erase` and `erase_add_single` now use explicit arguments. Co-authored-by: Johan Commelin <johan@commelin.net> Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com>
I am happy to remove some nolints for you!
* Define the product measure of two σ-finite measures. * Prove Tonelli's theorem. * Prove Fubini's theorem.
…uous.div` etc (#4667) Also add `continuous_on_(cos/sin)`.
The filter of complements to compact subsets.
…y` (#4584) Co-authored-by: Heather Macbeth <25316162+hrmacbeth@users.noreply.github.com> Co-authored-by: hrmacbeth <25316162+hrmacbeth@users.noreply.github.com>
…4595) Co-authored-by: Patrick Massot <patrickmassot@free.fr>
…4672) Also weaken some assumptions from a decidable linear order to a linear order.
This is trickier than it sounds because of a cyclic dependency. As a result we now have two versions of `prove_ne_zero` and `prove_clear_denom` is generic over them. One version proves ne using an order relation on the target, while the other uses `uncast` lemmas to reduce to `rat` and then uses the first `prove_ne_zero`. (This is why we actually want two versions - we can't solve this with a large mutual def, because it would result in an infinite recursion.)
We construct an order isomorphism between any two countable, nonempty, dense linear orders without endpoints, using the back-and-forth method.
I am happy to remove some nolints for you!
…at_bot` (#4878) * Redefine `at_top`/`at_bot` using `Ici`/`Iic`. * Add lemmas about `map`/`comap` of `at_top`/`at_bot` under `coe : s → α`, where `s` is one of `Ici a`, `Iic a`, `Ioi a`, `Iio a`.
Add `restrict_scalars` lemmas to `has_ftaylor_series_up_to_on`, `times_cont_diff_within_at`, `times_cont_diff_on`, `times_cont_diff_at`, and `times_cont_diff`.
* add `times_cont_diff_within_at_iff_forall_nat_le` and `times_cont_diff_on_iff_forall_nat_le`; * add `times_cont_diff_on_all_iff_nat` and `times_cont_diff_all_iff_nat`; * rename `times_cont_diff_at.differentiable` to `times_cont_diff_at.differentiable_at`; * add `times_cont_diff.div_const`; * add `times_cont_diff_succ_iff_deriv` * move some `of_le` lemmas up to support minor golfing of proofs.
…ebras are fields (#4903)
Some helpful lemmas for working with quantifiers, just other versions of what's already there.
#4690) Co-Authored-By: Rob Y. Lewis <rob.y.lewis@gmail.com> Co-authored-by: Vierkantor <vierkantor@vierkantor.com> Co-authored-by: Rob Lewis <Rob.y.lewis@gmail.com> Co-authored-by: Rob Lewis <rob.y.lewis@gmail.com>
Having a single character identifier in the root namespace is inconvenient. closes leanprover-community/doc-gen#83 Co-authored-by: Rob Lewis <rob.y.lewis@gmail.com>
I am happy to remove some nolints for you!
…om (#4888) Note that this required some stuff about polynomials to move to cut import cycles.
…er (#4907) Show that any small complete category has subsingleton homsets. Not sure if this is useful for anything - maybe it shouldn't be an instance
|
Thanks for picking this up! It looks like the build failed in your repo though: https://github.com/Ms2ger/mathlib/runs/1365821889 This is most likely due to a slow proof that was just fixed by #4920, so if you merge master again, it should work. |
bryangingechen
added
the
awaiting-author
|
@Ms2ger the diff is massive! Do you already have permission to push to branches on our repo? Because it would be much easier if you just work on the |
|
@jcommelin thanks for the invite, hopefully it's easier to review over in #773. |
Sign up for free
to subscribe to this conversation on GitHub.
Already have an account?
Sign in.
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.
Note: this is a PR to #773, not to master.