[Merged by Bors] - feat(data/{finset,finsupp,multiset}): more assorted lemmas #4006

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

Unfortunatley this can't be easily used to prove the polynomial version without polynomial induction

unfortunately this doesn't directly generalize to the polynomial version

…vectors2

rename a variable `boom` use `hp_prime` to refer to the assumption `fact p.prime`.

…stances (#3838) defines (new) `order_embedding` and `order_iso`, which map both < and <= replaces existing `rel_embedding` and `rel_iso` instances preserving < or <= with the new abbreviations

…ib into witt-vectors2

This is "progress" but maybe it should just all be reverted

but I'm still stuck on blur'

one goal is false so we need a new approach

Two R-module homs from finsupp X R which agree on `single x 1` agree everywhere. ``` lemma hom_ext [semiring β] [add_comm_monoid γ] [semimodule β γ] (φ ψ : (α →₀ β) →ₗ[β] γ) (h : ∀ a : α, φ (single a 1) = ψ (single a 1)) : φ = ψ ```

Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

Also add one lemma about `Inter`.

Main theorem is `set_has_maximal_iff_noetherian,` which relates well foundedness of `<` to being noetherian. Most notably a result of `well_founded.well_founded_iff_has_max'` provides the fact that on a partial ordering, `well_founded >` is equivalent to each nonempty set having a maximal element. `well_founded.well_founded_iff_has_min` provides an analogous fact for `well_founded <`. Some other miscellaneous lemmas are as follows `localization_map.integral_domain_of_local_at_prime` is the localization of an integral domain at a prime's complement is an integral domain `ideal.mul_eq_bot` is the fact that in an integral domain if I*J = 0, then at least one is 0. `submodule.nonzero_mem_of_gt_bot` is that if ⊥ < J, then J has a nonzero member. `lt_add_iff_not_mem` is that b is not a member of J iff J < J+(b). `bot_prime` states that 0 is a prime ideal of an integral domain. Co-authored-by: mushokunosora <knaka3435@gmail.com> Co-authored-by: mushokunosora <38799099+mushokunosora@users.noreply.github.com> Co-authored-by: Vierkantor <vierkantor@vierkantor.com>

Co-authored-by: Ashvni Narayanan <ashvni.n@gmail.com> Co-authored-by: Ashvni <ashvni.n@gmail.com> Co-authored-by: laughinggas <58670661+laughinggas@users.noreply.github.com>

…nction to be a homeomorphism (#3843) If a strictly monotone function between linear orders is surjective, it is a homeomorphism. If a strictly monotone function between conditionally complete linear orders is continuous, and tends to `+∞` at `+∞` and to `-∞` at `-∞`, then it is a homeomorphism. [Zulip discussion](https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there.20code.20for.20X.3F/topic/Order.20topology) Co-authored by: Yury Kudryashov <urkud@ya.ru> Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>

`is_integral_domain_iff_prime (I : ideal α) : is_integral_domain I.quotient ↔ I.is_prime`

@TwoFX

This is a second attempt (which works **much** better) at #3860, after @TwoFX explained how to do it properly. This PR takes the constructions of limits in the concrete categories `(Add)(Comm)[Mon|Group]`, `(Comm)(Semi)Ring`, `Module R`, and `Algebra R`, and makes sure that they never rely on the actual definitions of limits in "prior" categories. Of course, at this stage the `has_limit` typeclasses still contain data, so it's hard to judge whether we're really not relying on the definitions. I've marked all the `has_limits` instances in these files as irreducible, but the real proof is just that this same code is working over on the `prop_limits` branch. Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

@thjread

Co-authored by @thjread

Provide more API for `fin n`. Lemma names chosen to match equivalent lemmas in `nat`. Does not develop docstrings for the lemmas. New lemmas: iff lemmas for comparison `ne_iff_vne` `eq_mk_iff_coe_eq` `succ_le_succ_iff` `succ_lt_succ_iff` lemmas about explicit numerals `val_zero'` `mk_zero` `mk_one` `mk_bit0` `mk_bit1` `cast_succ_zero` `succ_zero_eq_one` `zero_ne_one` `pred_one` lemmas about order `zero_le` `succ_pos` `mk_succ_pos` `one_pos` `one_lt_succ_succ` `succ_succ_ne_one` `pred_mk_succ` `cast_succ_lt_last` `cast_succ_lt_succ` `lt_succ` `last_pos` `le_coe_last` coe lemmas: `coe_eq_cast_succ` `coe_succ_eq_succ` `coe_nat_eq_last` succ_above API: `succ_above_below` `succ_above_zero` `succ_above_last` `succ_above_above` `succ_above_pos` addition API: `add_one_pos` `pred_add_one` Co-authored by: Yury Kudryashov urkud@ya.ru Co-authored-by: Yakov Pechersky <pechersky@users.noreply.github.com>

I am happy to remove some nolints for you!

…: orthogonal projection hypotheses (#3952) As advised by Patrick in #3932, define `orthogonal_projection` (for both real inner product spaces and Euclidean affine spaces) without taking hypotheses of the subspace being nonempty and complete, defaulting to the identity map if those conditions are not satisfied, so making `orthogonal_projection` more convenient to use with those properties only being needed on lemmas but not simply to refer to the orthogonal projection at all. The hypotheses are removed from lemmas that don't need them because they are still true with the identity map. Some `nonempty` hypotheses are also removed where they follow from another hypothesis that gives a point or a nonempty set of points in the subspace. The unbundled `orthogonal_projection_fn` that's used only to prove properties needed to define a bundled linear or affine map still takes the original hypotheses, then a bundled map taking those hypotheses is defined under a new name, then that map is used to define plain `orthogonal_projection` which does not take any of those hypotheses and is the version expected to be used in all lemmas after it has been defined.

…imple graphs (#3672) defines the adjacency matrix of a simple graph proves lemmas about adjacency matrix that will form the bulk of the proof of the friendship theorem (freek 83) Co-authored-by: Aaron Anderson <awainverse@gmail.com>

Define the reflection of a point in an affine subspace, as a bundled isometry, in terms of the orthogonal projection onto that subspace, and prove some basic lemmas about it.

…a local predicate (#3906) Functions satisfying a local predicate form a sheaf. This sheaf has a natural map from the stalk to the original fiber, and we give conditions for this map to be injective or surjective. Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

…l functor (#3609) # Checking the sheaf condition on the underlying presheaf of types. If `G : C ⥤ D` is a functor which reflects isomorphisms and preserves limits (we assume all limits exist in both `C` and `D`), then checking the sheaf condition for a presheaf `F : presheaf C X` is equivalent to checking the sheaf condition for `F ⋙ G`. The important special case is when `C` is a concrete category with a forgetful functor that preserves limits and reflects isomorphisms. Then to check the sheaf condition it suffices to check it on the underlying sheaf of types. ## References * https://stacks.math.columbia.edu/tag/0073 Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

@rwbarton

…imits in `Type` (#3960) This is some work @rwbarton did last year. I've merged master, written some comments, and satisfied the linter. Co-authored-by: Reid Barton <rwbarton@gmail.com> Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

This PR gives a way to apply `ext` after `congr'`. `congr' 3 with x y : 2` is a new notation for `congr' 3; ext x y : 2`. New tactic `rcongr` that recursively keeps applying `congr'` and `ext`. Move `congr'` and every tactic depending on it from `tactic/interactive` to a new file `tactic/congr`. The original `tactic.interactive.congr'` is now best called as `tactic.congr'`. Other than the tactics `congr'` and `rcongr` no tactics have been (essentially) changed.

Add a subsingleton data structure expressing that a parallel pair of morphisms is a kernel pair of a given morphism. Another PR from my topos project. A pretty minimal API since I didn't need much there - I also didn't introduce anything like `has_kernel_pairs` largely because I didn't need it, but also because I don't know that it's useful for anyone, and it might conflict with ideas in the prop-limits branch.

fixes #3958 based on my completely unscientific test methods, this went from 40 seconds to ~~19~~ 17 seconds (on my laptop). What I've done here is just `squeeze_simp`, but further speedup is definitely possible. Suggestions for what to do with `simp [*, eq_inv_iff_eq] at * <|> cc` are welcome, and should speed this file up a bit more.

Add eigenspaces and eigenvalues of linear maps. Add lemma that in a finite-dimensional vector space over an algebraically closed field, eigenvalues exist. Add lemma that eigenvectors belonging to distinct eigenvalues are linearly independent. This is a rework of #3864, following Cyril's suggestion. Generalized eigenspaces will come in a subsequent PR.

I am happy to remove some nolints for you!

Use priority 100 for these `extends` instances.

…dered semimodules (#3931) This shows that a convex cone defines an ordered semimodule and vice-versa. Co-authored-by: Frédéric Dupuis <31101893+dupuisf@users.noreply.github.com>

@semorrison

* Misc. style cleanups and code golf * Changed naming and namespace to adhere more closely to the naming convention * Changed `impartial` to be a `class`. I am aware that @semorrison explicitly requested not to make `impartial` a class in the #3855, but after working with the definition a bit I concluded that making it a class is worth it, simply because writing `impartial_add (nim_impartial _) (nim_impartial _)` gets annoying quite quickly, but also because you tend to get goal states of the form `Grundy_value _ = Grundy_value _`. By making `impartial` a class and making the game argument explicit, these goal states look like `grundy_value G = grundy_value H`, which is much nicer to work with.

This defines the structure sheaf on Spec R, following Hartshorne, as a sheaf in `CommRing` on `prime_spectrum R`. We still need to show at the stalk at a point is just the localization; this is another page of Hartshorne, and will come in a subsequent PR. 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>

* Some `decidable.*` order theorems have been moved to core. * `fin` is now a subtype. This means that the whnf of `fin n` is now `{i // i < n}`. Also, the coercion `fin n → nat` is now preferred over `subtype.val`. The entire library has been refactored accordingly. (Although I probably missed some cases.) * `in_current_file'` was removed since the bug in `in_current_file` was fixed in core. * The syntax of `guard_hyp` in core was changed from `guard_hyp h := t` to `guard_hyp h : t`, so the syntax for the related `guard_hyp'`, `match_hyp` and `guard_hyp_strict` tactics in `tactic.interactive` was changed as well. Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com>

This backports some changes from the `prop_limits` branch. Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

From the sphere eversion project, define the determinant of a family of vectors with respects to a basis. The main result is `is_basis.iff_det` asserting a family of vectors is a basis iff its determinant in some basis is invertible. Also renames `equiv_fun_basis` to `is_basis.equiv_fun` and `equiv_fun_basis_symm_apply` to `is_basis.equiv_fun_symm_apply`, in order to use dot notation. Co-authored-by: Anne Baanen t.baanen@vu.nl Co-authored-by: Rob Lewis <Rob.y.lewis@gmail.com> Co-authored-by: Rob Lewis <rob.y.lewis@gmail.com>

…theorem (#3953) adds several assorted lemmas about matrices and `zmod p` proves that if `M` is a square matrix with entries in `zmod p`, then `tr M^p = tr M`, needed for friendship theorem Co-authored-by: Aaron Anderson <awainverse@gmail.com>

Add an instance `nontrivial (fin (n + 2))`.

…3977)

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.

…3962)

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>

Commits on May 8, 2020

WIP

jcommelin committed May 8, 2020

Configuration menu

View commit details

Copy full SHA for e30645b

Browse repository at this point

Copy the full SHA

e30645b View commit details

Browse the repository at this point in the history

Commits on May 19, 2020

Merge branch 'master' into witt-vectors2

jcommelin committed May 19, 2020

Configuration menu

View commit details

Copy full SHA for 7654579

Browse repository at this point

Copy the full SHA

7654579 View commit details

Browse the repository at this point in the history

Commits on May 20, 2020

WIP

jcommelin committed May 20, 2020

Configuration menu

View commit details

Copy full SHA for 091e47f

Browse repository at this point

Copy the full SHA

091e47f View commit details

Browse the repository at this point in the history

Commits on May 29, 2020

WIP

jcommelin committed May 29, 2020

Configuration menu

View commit details

Copy full SHA for aebec4b

Browse repository at this point

Copy the full SHA

aebec4b View commit details

Browse the repository at this point in the history

Commits on Jun 4, 2020

More abstraction

jcommelin committed Jun 4, 2020

Configuration menu

View commit details

Copy full SHA for e9279d6

Browse repository at this point

Copy the full SHA

e9279d6 View commit details

Browse the repository at this point in the history

Commits on Jun 8, 2020

trivial

jcommelin committed Jun 8, 2020

Configuration menu

View commit details

Copy full SHA for 09ac1af

Browse repository at this point

Copy the full SHA

09ac1af View commit details

Browse the repository at this point in the history

Commits on Jul 22, 2020

WIP

jcommelin committed Jul 22, 2020

Configuration menu

View commit details

Copy full SHA for 26bd3fb

Browse repository at this point

Copy the full SHA

26bd3fb View commit details

Browse the repository at this point in the history

Commits on Aug 13, 2020

clean up unused prime arguments

robertylewis committed Aug 13, 2020

Configuration menu

View commit details

Copy full SHA for 4a036d6

Browse repository at this point

Copy the full SHA

4a036d6 View commit details

Browse the repository at this point in the history

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[Merged by Bors] - feat(data/{finset,finsupp,multiset}): more assorted lemmas #4006

[Merged by Bors] - feat(data/{finset,finsupp,multiset}): more assorted lemmas #4006

Commits on May 7, 2020

Commits on May 8, 2020

Commits on May 12, 2020

Commits on May 19, 2020

Commits on May 20, 2020

Commits on May 21, 2020

Commits on May 28, 2020

Commits on May 29, 2020

Commits on May 30, 2020

Commits on Jun 1, 2020

Commits on Jun 2, 2020

Commits on Jun 3, 2020

Commits on Jun 4, 2020

Commits on Jun 6, 2020

Commits on Jun 8, 2020

Commits on Jul 20, 2020

Commits on Jul 21, 2020

Commits on Jul 22, 2020

Commits on Jul 24, 2020

Commits on Aug 2, 2020

Commits on Aug 8, 2020

Commits on Aug 13, 2020

Commits on Aug 17, 2020

Commits on Aug 18, 2020

Commits on Aug 19, 2020

Commits on Aug 20, 2020

Commits on Aug 21, 2020

Commits on Aug 24, 2020

Commits on Aug 25, 2020

Commits on Aug 26, 2020

Commits on Aug 27, 2020

Commits on Aug 28, 2020

Commits on Aug 29, 2020

Commits on Aug 30, 2020

Commits on Aug 31, 2020