[Merged by Bors] - feat(data/{finset,finsupp,multiset}): more assorted lemmas #4006
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
A lot of what remains is type class search failure. It is probably a good idea to bundle all the ring homs in sight.
A lot of what remains is type class search failure. It is probably a good idea to bundle all the ring homs in sight.
…ib into witt-vectors2
Add an instance `nontrivial (fin (n + 2))`.
Co-authored-by: jalex-stark <alexmaplegm@gmail.com> Co-authored-by: Frédéric Dupuis <31101893+dupuisf@users.noreply.github.com>
…up and nest. (#3764) this is a transplant of leanprover-community/lean#439 the relevant css section looks more or less like this: ```css .indent-code { text-indent: calc(var(--indent-level) * -1ch); padding-left: calc(var(--indent-level) * 1ch); } ``` For details, one can play around here: https://jsfiddle.net/xbzhL60m/45/ Co-authored-by: Ed Ayers <EdAyers@users.noreply.github.com> Co-authored-by: Gabriel Ebner <gebner@gebner.org> Co-authored-by: E.W.Ayers <E.W.Ayers@maths.cam.ac.uk>
Add a lemma that an injective function from a nontrivial type has an argument at which it does not take a given value.
Now you can hit a new button in the tooltip and it will reveal the definition location in the editor! Co-authored-by: Ed Ayers <EdAyers@users.noreply.github.com>
Add a `simp` lemma giving the range of `mono_of_fin`.
The definition of a `Scheme`, and the category of schemes as the full subcategory of locally ringed spaces. Co-authored-by: Johan Commelin <johan@commelin.net> Co-authored-by: Kevin Buzzard <k.buzzard@imperial.ac.uk> Co-authored-by: Scott Morrison <scott.morrison@gmail.com> Co-authored-by: Ashvni <ashvni.n@gmail.com>
This commit adds three induction principles for measure theory * To prove something for arbitrary simple functions * To prove something for arbitrary measurable functions into `ennreal` * To prove something for arbitrary measurable + integrable functions. This also adds some basic lemmas to various files. Not all of them are used in this PR, some will be used by near-future PRs. Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>
After the recent changes to make `fin n` a subtype, expressions involving `fin.mk` were not getting simplified as they used to be, since the `simp` lemmas are for the anonymous constructor, which is `subtype.mk` not `fin.mk`. Add a `simp` lemma converting `fin.mk` to the anonymous constructor. In particular, unsimplified expressions involving `fin.mk` were coming out of `fin_cases` (I think this comes from `fin_range` in `data/list/range.lean` using `fin.mk`). I don't know if that should be avoiding creating the `fin.mk` expressions in the first place, but simplifying them seems a good idea in any case.
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
… the quotient is a field (#3986) One half of the theorem was already proven (the implication maximal ideal implies that the quotient is a field), but the other half was not, mainly because it was missing a necessary predicate. I added the predicate is_field that can be used to tell Lean that the usual ring structure on the quotient extends to a field. The predicate along with proofs to move between is_field and field were provided by Kevin Buzzard. I also added a lemma that the inverse is unique in is_field. At the end I also added the iff statement of the theorem. Co-authored-by: AlexandruBosinta <32337238+AlexandruBosinta@users.noreply.github.com>
See https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/extension.20performance The bug seems to go away if we collapse the extra nested spans made by `block` in to one span. Still should do some tests to make sure this doesn't break anything else. Minimal breaking example is: ``` import tactic.interactive_expr example : 0+1+2+3+4+5+6+7+8+9 + 0+1+2+3+4+5+6+7+8+9 = 0+1+2+3+4+5+6+7+8+9 := by skip ``` Co-authored-by: Ed Ayers <EdAyers@users.noreply.github.com>
robertylewis
added
the
awaiting-review
|
bors merge |
github-actions
bot
added
ready-to-merge
bors bot
pushed a commit
that referenced
this pull request
Sep 1, 2020
Another grab bag of facts from the Witt vector branch. Coauthored by: Johan Commelin <johan@commelin.net> <!-- put comments you want to keep out of the PR commit here --> Co-authored-by: Johan Commelin <johan@commelin.net>
|
Pull request successfully merged into master. Build succeeded: |
bors
bot
changed the title
PatrickMassot
pushed a commit
that referenced
this pull request
Sep 8, 2020
Another grab bag of facts from the Witt vector branch. Coauthored by: Johan Commelin <johan@commelin.net> <!-- put comments you want to keep out of the PR commit here --> Co-authored-by: Johan Commelin <johan@commelin.net>
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.
Another grab bag of facts from the Witt vector branch.
Coauthored by: Johan Commelin johan@commelin.net