[Merged by Bors] - feat(algebra/big_operators/associated): dvd_prod_iff for finset and finsupp
#10675
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
stuart-presnell
added
the
awaiting-review
|
could you also make the |
eric-wieser
reviewed
Dec 9, 2021
eric-wieser
reviewed
Dec 9, 2021
eric-wieser
added
awaiting-author
stuart-presnell
added
awaiting-review
ericrbg
reviewed
Dec 9, 2021
ericrbg
added
awaiting-review
1 task
stuart-presnell
added
awaiting-author
stuart-presnell
added
awaiting-review
|
Since last comment the |
fpvandoorn
added
awaiting-author
Using `algebra/big_operators/associated.lean`
github-actions
bot
added
the
merge-conflict
github-actions
bot
removed
the
merge-conflict
stuart-presnell
changed the title
dvd_prod_iff for finset and finsuppdvd_prod_iff for finset and finsupp
Yes, I've moved everything into |
stuart-presnell
added
awaiting-review
|
bors merge |
github-actions
bot
added
ready-to-merge
|
Pull request successfully merged into master. Build succeeded: |
bors
bot
changed the title
dvd_prod_iff for finset and finsuppdvd_prod_iff for finset and finsupp
yuma-mizuno
added a commit
that referenced
this pull request
Jan 11, 2022
commit 2e003c9a7fff62c7f71ff4efda94571fe449fb8d
Author: Gabriel Ebner <gebner@gebner.org>
Date: Mon Jan 10 19:54:28 2022 +0000
feat(data/set/basic): add decidable instances for boolean operations (#11354)
Add decidability instances for `a ∈ s ∩ t`, etc.
commit 427e5b59b39319af0f2793a486e475bfbb7cedf6
Author: Stuart Presnell <stuart.presnell@gmail.com>
Date: Mon Jan 10 19:54:26 2022 +0000
feat(data/nat/factorization): Evaluating a multiplicative function over prime power divisors (#11167)
For any multiplicative function `f` with `f 1 = 1` and any `n > 0`, we can evaluate `f n` by evaluating `f` at `p ^ k` over the factorization of `n`.
Also provides an alternative version that swaps the `0 < n` condition for an extra `f 0 = 1` condition, as suggested by @ericrbg.
This allows a very simple proof that `n.factorization.prod pow = n`
commit dc3cbb7d7d31191be71a6a52015e03a7578ff961
Author: damiano <adomani@gmail.com>
Date: Mon Jan 10 16:17:20 2022 +0000
feat(data/polynomial/erase_lead): introduce two lemmas to compute `nat_degree`s under certain maps (#11265)
This PR is a step in the direction of simplifying #11139.
It contains a proof of the helper lemmas `map_nat_degree_eq_sub` and `map_nat_degree_eq_nat_degree` to shorten the proof of `nat_degree_hasse_deriv` and `nat_degree_taylor`.
[Zulip](https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/.2311139.20taylor.20sum.20and.20nat_degree_taylor)
commit 168ad7fc5d8173ad38be9767a22d50b8ecf1cd00
Author: Eric <ericrboidi@gmail.com>
Date: Mon Jan 10 16:17:19 2022 +0000
feat(data/nat/cast): generalize to `fun_like` (#11128)
commit 1533f158f7788de1a295f39b9cd2e5a4d720f279
Author: Bolton Bailey <bolton.bailey@gmail.com>
Date: Mon Jan 10 13:08:00 2022 +0000
feat(logic/basic): add eq_true_eq_id (#11341)
Adds the simp lemma `eq_true_eq_id : eq true = id`, a sort of curried version of `eq_true : (a = true) = a` in core.
commit fabc5101713f087e01ac66b6f2ae41b0a3357dfa
Author: Joseph Myers <jsm@polyomino.org.uk>
Date: Mon Jan 10 13:07:59 2022 +0000
feat(linear_algebra/determinant): `linear_equiv.det_conj` (#11340)
Add a version of the `linear_map.det_conj` lemma for `linear_equiv.det`.
commit 48b21e51f9ade29c814c1e0acaa8ed24cc48bb1f
Author: Kexing Ying <kexing.ying19@imperial.ac.uk>
Date: Mon Jan 10 13:07:57 2022 +0000
feat(probability_theory/martingale): one direction of the optional stopping theorem (#11007)
commit 7782157164780f05f50cb4dcde79267fd5877072
Author: Mantas Bakšys <baksys.mantas@gmail.com>
Date: Mon Jan 10 10:18:16 2022 +0000
feat (data/finset/lattice): add more finset induction lemmas (#10889)
2 more finset induction lemmas based on the order imposed by a function.
Co-authored-by: Mantas Bakšys <39908973+MantasBaksys@users.noreply.github.com>
Co-authored-by: Rob Lewis <Rob.y.lewis@gmail.com>
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
commit 99fe7acbf797b71f9374d109bc3761eab09d1a0f
Author: Eric Wieser <wieser.eric@gmail.com>
Date: Mon Jan 10 01:23:46 2022 +0000
chore(data/set/function): move inv_fun_on out of `logic/function/basic` (#11330)
This removes `function.inv_fun_on_eq'` as it is a duplicate of `inj_on.left_inv_on_inv_fun_on`.
commit 6a1093970ab41a193642f06b0de0e28f2918f54e
Author: Rob Lewis <Rob.y.lewis@gmail.com>
Date: Sun Jan 9 23:15:30 2022 +0000
fix(docs/references.bib): syntax error (#11342)
This broke the docs build.
commit ce17b657926068f969a8e0bf0cc1352f0f00f587
Author: Alex J Best <alex.j.best@gmail.com>
Date: Sun Jan 9 21:08:06 2022 +0000
feat(topology/algebra/monoid): to_additivize some lemmas (#11310)
Uncomment a commented out to additive line that looks like its been there
for 3 years (since
https://github.com/leanprover-community/mathlib/commit/581cf19bf1885ef874c39c9902a93f579bc8c22d)
The changes to to_additive in the past few years now make the
generated lemma useful.
Also to_additivize a bunch of other lemmas in this file.
commit d13b3a4a392ea7273dfa4727dbd1892e26cfd518
Author: Eric <ericrboidi@gmail.com>
Date: Sun Jan 9 18:06:11 2022 +0000
chore(*): update to 3.37.0c (#11325)
the major breaking change this version is making `default`'s parameters
implicit, as opposed to explicit. there was also some slight "free"
golfing due to the better `out_param` simp support.
commit 47a8d5a63cd90d13a9280fdb5f0fce3a7536d5b4
Author: Yaël Dillies <yael.dillies@gmail.com>
Date: Sun Jan 9 18:06:09 2022 +0000
refactor(data/{sigma,psigma}/order): Use `lex` synonym and new notation (#11235)
This introduces notations `Σₗ i, α i` and `Σₗ' i, α i` for `lex (Σ i, α i)` and `lex (Σ' i, α i)` and use them instead of the instance switch with locale `lex`.
commit 2bb25f05603d7fb79704fe705b3e25ff47a5e674
Author: Joseph Myers <jsm@polyomino.org.uk>
Date: Sun Jan 9 16:18:25 2022 +0000
feat(algebra/periodic): lifting to function on quotient group (#11321)
I want to make more use of the type `real.angle` in
`analysis.special_functions.trigonometric.angle`, including defining
functions from this type in terms of periodic functions from `ℝ`. To
support defining such functions, add a definition `periodic.lift` that
lifts a periodic function from `α` to a function from
`α ⧸ (add_subgroup.zmultiples c)`, along with a lemma
`periodic.lift_coe` about the values of the resulting function.
commit 49ba33e552ebe03482bd613e8264d88dbec2b040
Author: Alex J Best <alex.j.best@gmail.com>
Date: Sun Jan 9 16:18:24 2022 +0000
feat(vscode): add a snippet for inserting a module docstring template (#11312)
We already have a vscode snippet for adding copyright headers, this PR adds a similar one to generate a default module docstring with many of the common sections stubbed out.
By default it takes the filename, converts underscores to spaces and capitalizes each word to create the title, as this seems a sensible default. But otherwise all text is a static default example following the documentation style page to make it easier to remember the various recommended secitons.
To test do `ctrl+shift+p` to open the command pallette, type insert snippet, enter, and type module and it should show up.
See also #3186
commit fadbd9599176e9076e477b0843dd3adb93c6a568
Author: Yakov Pechersky <ffxen158@gmail.com>
Date: Sun Jan 9 16:18:23 2022 +0000
feat(field_theory/ratfunc): ratfunc.lift_on without is_domain (#11227)
We might want to state results about rational functions without assuming
that the base ring is an integral domain.
Cf. Misconceptions about $K_X$, Kleiman, Steven; Stacks01X1
Co-authored-by: Yakov Pechersky <ypechersky@treeline.bio>
commit 9c224ff6747a08ce8093289f4243ff2513072c21
Author: Yaël Dillies <yael.dillies@gmail.com>
Date: Sun Jan 9 13:09:57 2022 +0000
split(data/set/functor): Split off `data.set.lattice` (#11327)
This moves the functor structure of `set` in a new file `data.set.functor`.
Also adds `alternative set` because it's quick and easy.
commit ad4ea53813e6895892ddca0b9ede7a5e47e0b836
Author: Alex J Best <alex.j.best@gmail.com>
Date: Sun Jan 9 07:58:15 2022 +0000
chore(*): miscellaneous to_additive related cleanup (#11316)
A few cleanup changes related to to_additive:
* After https://github.com/leanprover-community/lean/pull/618 was merged, we no longer need to add namespaces manually in filtered_colimits and open subgroup
* to_additive can now generate some more lemmas in big_operators/fin
* to_additive now handles a proof in measure/haar better than it used to
so remove a workaround there
commit ca5e55ccca174a096a8126d7053b0918a569214c
Author: Joseph Myers <jsm@polyomino.org.uk>
Date: Sun Jan 9 06:06:07 2022 +0000
feat(linear_algebra/basis): `basis.ext`, `basis.ext'` for semilinear maps (#11317)
Extend `basis.ext` and `basis.ext'` to apply to the general
(semilinear) case of `linear_map` and `linear_equiv`.
commit a58553d58d4019ea4a6815a25b964d2963ed0928
Author: Stuart Presnell <stuart.presnell@gmail.com>
Date: Sun Jan 9 03:54:54 2022 +0000
feat(data/nat/factorization): Add lemmas on factorizations of pairs of coprime numbers (#10850)
commit d4846b32a88c9f0e6a5000da901b07e56f5ae7ac
Author: Eric <ericrboidi@gmail.com>
Date: Sun Jan 9 01:21:32 2022 +0000
chore(ring_theory/fractional_ideal): fix typo (#11311)
commit 22ff4ebc9bd521cc075fb5f87d55d6d029997e73
Author: Arthur Paulino <arthurleonardo.ap@gmail.com>
Date: Sat Jan 8 23:10:53 2022 +0000
feat(combinatorics/simple_graph/matchings): even_card_vertices_of_perfect_matching (#11083)
Co-authored-by: YaelDillies <yael.dillies@gmail.com>
commit 0a75fdfb102a8a00f5a81fc97aad330d1ba444bd
Author: Jireh Loreaux <loreaujy@gmail.com>
Date: Sat Jan 8 21:54:48 2022 +0000
feat(linear_algebra/eigenspace): prove eigenvalues are exactly elements of the spectrum when the space is finite dimensional (#10961)
This adds `has_eigenvalue_iff_mem_spectrum` and then uses it to golf `exists_eigenvalue`
- [x] depends on: #10912
- [x] depends on: #10919
Co-authored-by: Vierkantor <vierkantor@vierkantor.com>
commit ee136d903b12de0474236113577b7ab001a1c7f0
Author: Eric Wieser <wieser.eric@gmail.com>
Date: Sat Jan 8 18:36:59 2022 +0000
chore(set_theory/game/domineering): extract repeated goal into lemma and golf (#11298)
`fst_pred_mem_erase_of_mem_right` and `snd_pred_mem_erase_of_mem_left` were common subgoals that appeared in two lemmas each.
commit 84dbe31db27f908325b3f302ec5f5f2e145b2c2a
Author: Floris van Doorn <fpvdoorn@gmail.com>
Date: Sat Jan 8 18:36:57 2022 +0000
feat(topology/basic): add explicit definition of continuous_at (#11296)
This was convenient in a demo.
commit 25704cac29f50cd0e92c2c5a0a9cabc7d9f86f18
Author: Rob Lewis <Rob.y.lewis@gmail.com>
Date: Sat Jan 8 18:36:56 2022 +0000
docs(algebra/covariant_and_contravariant): minor typos (#11293)
commit 09f698902747299a650bdb94546f14ee7b7b3b26
Author: Yury G. Kudryashov <urkud@urkud.name>
Date: Sat Jan 8 18:36:54 2022 +0000
chore(analysis/normed_space/banach): move more to the `continuous_linear_map` NS (#11263)
## Rename
* `open_mapping` → `continuous_linear_map.is_open_map`;
* `open_mapping_affine` → `affine_map.is_open_map`;
### New lemmas
* `continuous_linear_map.quotient_map`,
* `continuous_linear_map.interior_preimage`,
* `continuous_linear_map.closure_preimage`,
* `continuous_linear_map.frontier_preimage`.
commit 60e279ba2bfe69f937b5f69b110a440538b8f6a5
Author: Eric <ericrboidi@gmail.com>
Date: Sat Jan 8 18:36:52 2022 +0000
chore(*): update to lean 3.36.0 (#11253)
The main breaking change is the change in elaboration of double membership binders into x hx y hy, from x y hx hy.
Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>
commit dd1242d2aec84561c8f8651721ea1c1d8d25007a
Author: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>
Date: Sat Jan 8 16:29:06 2022 +0000
feat(algebra/associated): generalize nat.prime.pow_dvd_of_dvd_mul_{left,right} (#11301)
commit c76e11366b91541c43f547f693f444e510a5d444
Author: Yakov Pechersky <ypechersky@treeline.bio>
Date: Sat Jan 8 16:29:05 2022 +0000
feat(ring_theory/laurent): coercion of R[x] to R((x)) lemmas (#11295)
Make the coercion be `simp`-normal as opposed to `(algebra_map _ _)`.
Also generalize `of_power_series Γ R (power_series.C R r) = hahn_series.C r` and similarly for `X` to be true for any `[ordered semiring Γ]`, not just `ℤ`.
commit 116250977f0b8d9d42fde47709faa3a61d2b833d
Author: Eric Wieser <wieser.eric@gmail.com>
Date: Sat Jan 8 16:29:04 2022 +0000
chore(data/fin/vec_notation): generalize smul_cons (#11285)
commit 56f021a94c4bc52b567abb3b4bae4718896e0d0c
Author: damiano <adomani@gmail.com>
Date: Sat Jan 8 16:29:01 2022 +0000
feat(data/polynomial/{erase_lead + denoms_clearable}): strengthen a lemma (#11257)
This PR is a step in the direction of simplifying #11139 .
It strengthens lemma `induction_with_nat_degree_le` by showing that restriction can be strengthened on one of the assumptions.
~~It proves a lemma computing the `nat_degree` under functions on polynomials that include the shift of a variable.~~
EDIT: the lemma was moved to the later PR #11265.
It fixes the unique use of lemma `induction_with_nat_degree_le`.
[Zulip discussion](https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/.2311139.20taylor.20sum.20and.20nat_degree_taylor)
commit b181a12035a565e4162372a414d0bc793c8e6bfb
Author: David Wärn <codwarn@gmail.com>
Date: Sat Jan 8 16:28:59 2022 +0000
refactor(combinatorics/quiver): split into several files (#11006)
This PR splits `combinatorics/quiver.lean` into several files. The main reason for this is to ensure that the category theory library only imports the necessary definitions (and not for example the stuff on arborescences).
Also adds some more documentation, and fixes a bug in the definition of weakly connected components.
commit 9b3fec5511f0c545e06e315051a4379dcbe3fa8a
Author: Junyan Xu <junyanxumath@gmail.com>
Date: Sat Jan 8 16:28:58 2022 +0000
feat(algebraic_geometry): Gamma-Spec adjunction (#9802)
Define the adjunction between the functors Gamma (global sections) and Spec (to LocallyRingedSpace).
I'm currently working on a more general version in http://arxiv.org/pdf/1103.2139.pdf (Theorem 2), which may require refactoring `structure_sheaf` and `Spec`.
Co-authored-by: erd1 <the.erd.one@gmail.com>
commit b1955dcaac4bd7ce126c3466b251fd13557ece1d
Author: Martin Dvořák <dvorakmartinbridge@seznam.cz>
Date: Sat Jan 8 15:04:37 2022 +0000
feat(data/matrix/basic): infix notation for matrix.dot_product in locale matrix (#11289)
I created an infix notation for `matrix.dot_product` in locale `matrix`. The notation was consulted with @eric-wieser in #11181.
Co-authored-by: Martin Dvořák <martin.dvorak@matfyz.cz>
commit 43041277d34b62a15c8cf53a27832fd8cd3151e1
Author: Alex J Best <alex.j.best@gmail.com>
Date: Sat Jan 8 15:04:36 2022 +0000
feat(ring_theory/power_series): teach simp to simplify more coercions of polynomials to power series (#11287)
So that simp can prove that the polynomial `5 * X^2 + X + 1` coerced to a power series is the same thing with the power series generator `X`. Likewise for `mv_power_series`.
commit e8713864f6265686bc33f41d368a6cc32887a1e6
Author: Riccardo Brasca <riccardo.brasca@gmail.com>
Date: Sat Jan 8 15:04:35 2022 +0000
feat(number_theory/cyclotomic/basic): add lemmas (#11264)
From flt-regular.
commit c7fa66eac25cfdb52638a590cfcf372dd2c18415
Author: Bhavik Mehta <bhavikmehta8@gmail.com>
Date: Sat Jan 8 15:04:33 2022 +0000
feat(data/nat/prime): power to factor count divides natural (#11226)
commit 4d79d5fe60257cd44669db5a0e7c910101fb92cf
Author: Rémy Degenne <Remydegenne@gmail.com>
Date: Sat Jan 8 15:04:32 2022 +0000
chore(measure_theory/group/arithmetic): use implicit argument for measurable_space (#11205)
The `measurable_space` argument is inferred from other arguments (like `measurable f` or a measure for example) instead of being a type class. This ensures that the lemmas are usable without `@` when several measurable space structures are used for the same type.
Also use more `variables`.
commit 22311732a26f101b6db8157cfea22becdffab464
Author: tb65536 <tb65536@uw.edu>
Date: Sat Jan 8 14:24:00 2022 +0000
feat(group_theory/commuting_probability): New file (#11243)
This PR introduces commuting probabilities of finite groups.
commit 07f9b8e1e71cfbba2ea1fa7f02eb7b9201fcebb6
Author: Yaël Dillies <yael.dillies@gmail.com>
Date: Sat Jan 8 07:22:54 2022 +0000
feat(data/sum/order): Linear and disjoint sums of orders (#11157)
This defines the disjoint sum of two orders on `α ⊕ β` and the linear (aka lexicographic) sum of two orders on `α ⊕ₗ β` (a type synonym of `α ⊕ β`) in a new file `data.sum.order`.
commit 303e77c8c0bfb81ee91b997fcc426e13701a9756
Author: Floris van Doorn <fpvdoorn@gmail.com>
Date: Sat Jan 8 00:14:42 2022 +0000
feat(topology/metric_space/hausdorff_distance): make iffs (#11288)
* Make `exists_edist_lt_of_inf_edist_lt` and `exists_dist_lt_of_inf_edist_lt` iffs. Rename to `inf_[e]dist_lt_iff`.
* Simplify some proofs
commit 5cbfddd3cb801f853bc840f9c353fdcd3b717623
Author: Yaël Dillies <yael.dillies@gmail.com>
Date: Fri Jan 7 18:21:53 2022 +0000
feat(data/finset/sym): Symmetric powers of a finset (#11142)
This defines `finset.sym` and `finset.sym2`, which are the `finset` analogs of `sym` and `sym2`, in a new file `data.finset.sym`.
commit a8d37c1d1a8c91a42a68715fc760f5136dcf980f
Author: Stuart Presnell <stuart.presnell@gmail.com>
Date: Fri Jan 7 18:21:52 2022 +0000
feat(data/nat/factorization): Defining `factorization` (#10540)
Defining `factorization` as a `finsupp`, as discussed in
https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/Prime.20factorizations
and
https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/Proof.20of.20Euler's.20product.20formula.20for.20totient
This is the first of a series of PRs to build up the infrastructure needed for the proof of Euler's product formula for the totient function.
commit 3b02ad77937a52a017612f76a6ee686d24c2ae0b
Author: Shing Tak Lam <shingtaklam1324@gmail.com>
Date: Fri Jan 7 18:21:50 2022 +0000
feat(topology/homotopy/equiv): Add homotopy equivalences between topological spaces (#10529)
commit 13e99c70cb53e79b25605752f4f73438927d98d5
Author: Eric Wieser <wieser.eric@gmail.com>
Date: Fri Jan 7 16:25:53 2022 +0000
feat(algebra,linear_algebra,ring_theory): more is_central_scalar instances (#11297)
This provides new transitive scalar actions:
* on `lie_submodule R L M` that match the actions on `submodule R M`
* on quotients by `lie_submodule R L M` that match the actions on quotients by `submodule R M`
The rest of the instances in this PR live in `Prop` so do not define any further actions.
This also fixes some overly verbose instance names.
commit b8f5d0acd62e251bc393da0a2054b50ddf6df2c4
Author: Adam Topaz <github@adamtopaz.com>
Date: Fri Jan 7 16:25:52 2022 +0000
chore(category_theory/abelian/basic): abelian categories have finite limits and finite colimits. (#11271)
commit b430316847d7aa4ff239f09f8436a310a8b7aabe
Author: Eric Wieser <wieser.eric@gmail.com>
Date: Fri Jan 7 14:24:20 2022 +0000
chore(topology/algebra/module/basic): add continuous_linear_map.is_central_scalar (#11291)
commit 3b7a783fc66c7e5c55b244ccb2c3d7d64bd8ec19
Author: Andrew Yang <the.erd.one@gmail.com>
Date: Fri Jan 7 14:24:17 2022 +0000
feat(topology/*): Gluing topological spaces (#9864)
Co-authored-by: erdOne <36414270+erdOne@users.noreply.github.com>
Co-authored-by: Adam Topaz <github@adamtopaz.com>
commit 6fb638b3e0e8d5c37319e9a6a71c08bf8b397120
Author: Yury G. Kudryashov <urkud@urkud.name>
Date: Fri Jan 7 12:43:41 2022 +0000
feat(*): add lemmas, golf (#11294)
### New lemmas
* `function.mul_support_nonempty_iff` and `function.support_nonempty_iff`;
* `set.infinite_union`;
* `nat.exists_subseq_of_forall_mem_union` (to be used in an upcoming mass golfing of `is_pwo`/`is_wf`);
* `hahn_series.coeff_inj`, `hahn_series.coeff_injective`, `hahn_series.coeff_fun_eq_zero_iff`, `hahn_series.support_eq_empty_iff`;
* `nat.coe_order_embedding_of_set` (`simp` + `rfl`);
* `nat.subtype.of_nat_range`, `nat.subtype.coe_comp_of_nat_range`.
### Golfed proofs
* `set.countable.prod`;
* `nat.order_embedding_of_set_range`;
* `hahn-series.support_nonempty_iff`;
### Renamed
* `set.finite.union_iff` → `set.finite_union`, add `@[simp]` attr;
* `set.finite.diff` → `set.finite.of_diff`, drop 1 arg;
commit 0b9663036339f050000277c99fab463b2e610f58
Author: Eric Wieser <wieser.eric@gmail.com>
Date: Thu Jan 6 19:34:08 2022 +0000
feat(algebra/{monoid_algebra/basic,free_non_unital_non_assoc_algebra,lie/free}): generalize typeclasses (#11283)
This fixes a number of missing or problematic typeclasses:
* The smul typeclasses on `monoid_algebra` had overly strong assumptions
* `add_comm_group (monoid_algebra k G)` was missing.
* `monoid_algebra` had diamonds in its int-module structures, which were different between the one inferred from `ring` and `add_group`.
* `monoid_algebra` was missing an instance of the new `non_unital_non_assoc_ring`.
* `free_non_unital_non_assoc_algebra` was missing a lot of smul typeclasses and transitive module structures that it should inherit from `monoid_algebra`. Since every instance should just be inherited, we change `free_non_unital_non_assoc_algebra` to an abbreviation.
* `free_lie_algebra` had diamonds in its int-module and nat-module structures.
* `free_lie_algebra` was missing transitive module structures.
This also golfs some proofs about `free_non_unital_non_assoc_algebra`, and removes the `irreducible` attributes since these just make some obvious proofs more awkward.
commit d0bf8bd244afa0d8d89732d35a04bd64b67e8e63
Author: Yaël Dillies <yael.dillies@gmail.com>
Date: Thu Jan 6 17:51:55 2022 +0000
feat(set_theory/ordinal): `ordinal` is a successor order (#11284)
This provides the `succ_order` instance for `ordinal`.
commit 5893fbfc0cd0218acc6362628c093d25f043abad
Author: damiano <adomani@gmail.com>
Date: Thu Jan 6 17:51:52 2022 +0000
feat(data/polynomial/monic): add two lemmas on degrees of monic polynomials (#11259)
This PR is a step in the direction of simplifying #11139.
The two lemmas involve computing the degree of a power of monic polynomials.
[Zulip](https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/.2311139.20taylor.20sum.20and.20nat_degree_taylor)
commit 9b39ab2a29fa9e81aef5c2fb228f4b19689d5cf8
Author: Yaël Dillies <yael.dillies@gmail.com>
Date: Thu Jan 6 14:41:11 2022 +0000
feat(algebra/group/freiman): Freiman homomorphisms (#10497)
This defines Freiman homomorphisms, which are maps preserving products of `n` elements (but only in the codomain. One can never get back to the domain).
This is useful in additive combinatorics.
commit d2428fae765f16ca2d044c6402b3c7755110f4d9
Author: Andrew Yang <the.erd.one@gmail.com>
Date: Thu Jan 6 12:39:56 2022 +0000
feat(ring_theory/localization): Localization is the localization of localization. (#11145)
Co-authored-by: Andrew Yang <36414270+erdOne@users.noreply.github.com>
Co-authored-by: Johan Commelin <johan@commelin.net>
commit 54c2567d817c19ecc2d018c0b1676df8b1d6cfea
Author: Andrew Yang <the.erd.one@gmail.com>
Date: Thu Jan 6 10:39:24 2022 +0000
feat(category_theory/sites): The pushforward pullback adjunction (#11273)
Co-authored-by: Andrew Yang <36414270+erdOne@users.noreply.github.com>
commit 7af5e86c7b8ecec06057f7b6da46606f790e2f6c
Author: Yaël Dillies <yael.dillies@gmail.com>
Date: Thu Jan 6 10:39:23 2022 +0000
feat(algebra/big_operators/multiset): Multiset product under some usual maps (#10907)
Product of the image of a multiset under `λ a, (f a)⁻¹`, `λ a, f a / g a`, `λ a, f a ^ n` (for `n` in `ℕ` and `ℤ`).
commit c391512eeb819045ccf03edc07d471bef758ebd9
Author: Heather Macbeth <25316162+hrmacbeth@users.noreply.github.com>
Date: Thu Jan 6 09:57:30 2022 +0000
feat(topology/metric_space/kuratowski): make the Kuratowski embedding have codomain the "true" ℓ^∞(ℕ) (#11280)
(Previously, we didn't have the "true" ℓ^∞(ℕ), so we used the space of bounded continuous functions on `ℕ` equipped with the discrete topology.)
commit f07f87e9d56081e84ff7130f3623fdd093a6eafe
Author: Yakov Pechersky <ypechersky@treeline.bio>
Date: Thu Jan 6 07:55:41 2022 +0000
feat(ring_theory/power_series/basic): algebra, solving TODOs (#11267)
`algebra (mv_polynomial σ R) (mv_power_series σ A)`
`algebra (mv_power_series σ R) (mv_power_series σ A)`
`algebra (polynomial R) (power_series A)`
`algebra (power_series R) (power_series A)`
`coe_to_mv_power_series.alg_hom`
`coe_to_power_series.alg_hom`
And API about the injectivity of coercions
commit 6952172934a8da662daa08d90753be596cdc98a1
Author: Yakov Pechersky <ffxen158@gmail.com>
Date: Thu Jan 6 07:55:40 2022 +0000
feat(data/nat/digits): digits_len (#11187)
Via a new `data.nat.log` import.
Also unprivate `digits_eq_cons_digits_div`.
The file needs a refactor to make the names more mathlib-like,
otherwise I would have named it `length_digits`.
commit b3260f37e534430ea20630d2a7130e33a010a152
Author: sgouezel <sebastien.gouezel@univ-rennes1.fr>
Date: Thu Jan 6 07:05:28 2022 +0000
feat(measure_theory/constructions/borel_space): new lemma tendsto_measure_cthickening (#11009)
Prove that, when `r` tends to `0`, the measure of the `r`-thickening of a set `s` tends to the measure of `s`.
commit 9f28b5d4deaba1f87b1b8f50a380570d5578c6fb
Author: Rob Lewis <Rob.y.lewis@gmail.com>
Date: Wed Jan 5 23:45:35 2022 +0000
chore(ci): update some workflows to use custom bot token (#11274)
Co-authored-by: Rob Lewis <rob.y.lewis@gmail.com>
commit e7189651b50ecb21c63e96ffacfd20c8fee1102c
Author: Oliver Nash <github@olivernash.org>
Date: Wed Jan 5 23:45:33 2022 +0000
feat(topology/uniform_space/compact_convergence): when the domain is compact, compact convergence is just uniform convergence (#11262)
commit a7611b2ce9c9f9617a8c8cea60027c605d464ddb
Author: Johan Commelin <johan@commelin.net>
Date: Wed Jan 5 23:45:32 2022 +0000
chore(*): notation for `units` (#11236)
commit cac4e196cd120396caf5b2faaf32ab3d5fb1ef08
Author: Violeta Hernández <vi.hdz.p@gmail.com>
Date: Wed Jan 5 23:45:31 2022 +0000
feat(set_theory/ordinal_arithmetic): Proved characterization of `log` (#11192)
As well as a few simple missing lemmas.
commit b67857e7892dfab8150aade5f65ca3532a568f5a
Author: Violeta Hernández <vi.hdz.p@gmail.com>
Date: Wed Jan 5 23:45:29 2022 +0000
refactor(set_theory/ordinal_arithmetic): Reworked `sup` and `bsup` API (#11048)
This PR does two things:
- It reworks and matches, for the most part, the API for `ordinal.sup` and `ordinal.bsup`.
- It introduces `ordinal.lsub` and `ordinal.blsub` for (bounded) least strict upper bounds, and proves the expected results.
commit 771d1449047288217cbfb845630f1bc943e5a83c
Author: Heather Macbeth <25316162+hrmacbeth@users.noreply.github.com>
Date: Wed Jan 5 22:31:56 2022 +0000
feat(analysis/normed_space/lp_space): completeness of the lp space on `Π i, E i` (#11094)
commit 8b2d181557c31eb2c7cf9f16ca8634bef82f12f1
Author: Yakov Pechersky <ffxen158@gmail.com>
Date: Wed Jan 5 19:08:16 2022 +0000
feat(ring_theory/laurent_series): laurent_series is_fraction_ring over power_series (#11220)
Co-authored-by: Johan Commelin <johan@commelin.net>
Co-authored-by: Yakov Pechersky <ypechersky@treeline.bio>
commit f6dfea6747135a0766aff67ded336b8556b8165e
Author: Yury G. Kudryashov <urkud@urkud.name>
Date: Wed Jan 5 17:28:18 2022 +0000
feat(measure_theory/integral): Cauchy integral formula for a circle (#10000)
commit 6bf904185616c3c3dfe21a916704724ba76c417c
Author: Eric Wieser <wieser.eric@gmail.com>
Date: Wed Jan 5 16:16:53 2022 +0000
doc(analysis/normed/group/basic): show notation in the typeclass docstring (#11260)
commit 3ab1c1cb53b5a2ceb6d209bad77dc9d4f5c744ee
Author: Alex J Best <alex.j.best@gmail.com>
Date: Wed Jan 5 16:16:51 2022 +0000
feat(algebra/polynomial/big_operators): lemmas about polynomial degree of products (#11258)
These already existed for `nat_degree` but `degree` versions seemed missing.
from flt-regular
commit a1f4ac35b18328d81e4b5bf9324b133a9e932a7e
Author: Yury G. Kudryashov <urkud@urkud.name>
Date: Wed Jan 5 16:16:50 2022 +0000
chore(topology): move 3 files to `topology/algebra/module/` (#11242)
commit 9fd7a02d03ba2ea9786eea4bf547b2c51e56ed6a
Author: Adam Topaz <github@adamtopaz.com>
Date: Wed Jan 5 14:15:46 2022 +0000
feat(category_theory/sites/left_exact): Sheafification is left exact. (#11252)
commit a580727103b75288890a37f68f8cb61613e4fddb
Author: Yury G. Kudryashov <urkud@urkud.name>
Date: Wed Jan 5 14:15:44 2022 +0000
chore(topology/omega_complete_partial_order): golf (#11250)
commit 802f23cf22b2b504ab7fc1fb495df00ef4444d88
Author: tb65536 <tb65536@uw.edu>
Date: Wed Jan 5 14:15:40 2022 +0000
feat(data/fintype/basic): `set_fintype_card_eq_univ_iff` (#11244)
Adds companion lemma to `set_fintype_card_le_univ`. This PR also moves several `set.to_finset` lemmas earlier in the file.
commit b27e33a0b2e32d9991e43cb6b2c47033e2f61988
Author: Eric Wieser <wieser.eric@gmail.com>
Date: Wed Jan 5 14:15:39 2022 +0000
feat(data/{fin/vec_notation, matrix/notation}): `cons_{add,sub,dot_product}_cons` (#11241)
While these can be proved by `simp`, they are not rejected by the simp linter.
commit 98b64f49f75d09f02f22138b72638198a64850be
Author: Joseph Myers <jsm@polyomino.org.uk>
Date: Wed Jan 5 14:15:38 2022 +0000
feat(linear_algebra/orientation): bases from orientations (#11234)
Add a lemma giving the orientation of a basis constructed with
`units_smul`, and thus definitions and lemmas to construct a basis
from an orientation.
commit 33b5d264b1c842fcb2149c72c7a21ee263d1af48
Author: Yury G. Kudryashov <urkud@urkud.name>
Date: Wed Jan 5 14:15:37 2022 +0000
feat(analysis/complex): `re`, `im`, and `closure`/`interior`/`frontier` (#11215)
commit 3115ced1ab3ff7610e55a9d4c52309fd09b251df
Author: Yakov Pechersky <ffxen158@gmail.com>
Date: Wed Jan 5 14:15:35 2022 +0000
feat(ring_theory/non_zero_divisors): mul_{left,right}_cancel API (#11211)
Not all `monoid_with_zero` are `cancel_monoid_with_zero`,
so we can't use `mul_right_cancel₀` everywhere. However, by definition,
multiplication by non-zero-divisors is 0 iff the multiplicand is 0.
In the context of a ring, that allows us to `mul_cancel_right`
Co-authored-by: Yakov Pechersky <ypechersky@treeline.bio>
commit 3bd2044b1a23157374a81d1f561c0c7991ddad3a
Author: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>
Date: Wed Jan 5 14:15:34 2022 +0000
chore(data/nat/prime): reuse a result from algebra.big_operators.associated (#11143)
commit 57a9f8beef9f565ca7ffdca58452394f866b239f
Author: Eric Wieser <wieser.eric@gmail.com>
Date: Wed Jan 5 14:15:33 2022 +0000
chore(group_theory/sub{monoid,group}, linear_algebra/basic): rename equivalences to mapped subobjects (#11075)
This makes the names shorter and more uniform:
* `add_equiv.map_add_submonoid`
* `add_equiv.map_add_subgroup`
* `linear_equiv.map_submodule`
commit 7e5eebd709744ab0ba21bf585cec6c356daa1e69
Author: Eric Wieser <wieser.eric@gmail.com>
Date: Wed Jan 5 14:15:32 2022 +0000
feat(linear_algebra/clifford_algebra/equivs): There is a clifford algebra isomorphic to the dual numbers (#10730)
This adds a brief file on the dual numbers, and then shows that they are equivalent to the clifford algebra with `Q = (0 : quadratic_form R R)`.
commit cef325863d264a4673799f391d5ca2d24269e897
Author: Eric Wieser <wieser.eric@gmail.com>
Date: Wed Jan 5 12:21:49 2022 +0000
chore(group_theory/group_action/defs): add instances to copy statements about left actions to right actions when the two are equal (#10949)
While these instances are usually available elsewhere, these shortcuts can reduce the number of typeclass assumptions other lemmas needs.
Since the instances carry no data, the only harm they can cause is performance.
There were some typeclass loops brought on by some bad instance unification, similar to the ones removed by @Vierkantor in 9ee2a50aa439d092c8dea16c1f82f7f8e1f1ea2c. We turn these into `lemma`s and duplicate the docstring explaining the problem. That commit has a much longer explanation of the problem.
commit 8d5830e62bc64643b055930055bf800722f8afa8
Author: Rémy Degenne <Remydegenne@gmail.com>
Date: Wed Jan 5 11:32:02 2022 +0000
chore(measure_theory/measurable_space): use implicit measurable_space argument (#11230)
The `measurable_space` argument is inferred from other arguments (like `measurable f` or a measure for example) instead of being a type class. This ensures that the lemmas are usable without `@` when several measurable space structures are used for the same type.
Co-authored-by: Rémy Degenne <remydegenne@gmail.com>
commit 4912740a5e08fd88caf25988be5bdb562323b8fb
Author: Heather Macbeth <25316162+hrmacbeth@users.noreply.github.com>
Date: Wed Jan 5 08:10:47 2022 +0000
chore(analysis/inner_product_space/basic): extract common `variables` (#11214)
Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>
commit b72d2ab218183aabf5d219bfc1d7742f3fffc73f
Author: Christopher Hoskin <christopher.hoskin@gmail.com>
Date: Wed Jan 5 08:10:46 2022 +0000
feat(algebra/ring/basic): Introduce non-unital, non-associative rings (#11124)
Adds the class `non_unital_non_assoc_ring` to `algebra.ring.basic` to represent rings which are not assumed to be unital or associative and shows that (unital, associative) rings are instances of `non_unital_non_assoc_ring`.
Needed by #11073.
Co-authored-by: Christopher Hoskin <mans0954@users.noreply.github.com>
Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>
commit 58b1429a0ef2390cae0d10afc060049badcd0718
Author: Yury G. Kudryashov <urkud@urkud.name>
Date: Wed Jan 5 06:18:07 2022 +0000
chore(algebra/group/pi): `pow_apply` can be `rfl` (#11249)
commit 4093834bfa35d40c0ee2a7d7336b9fe54ff66e5c
Author: kkytola <kalle.kytola@aalto.fi>
Date: Wed Jan 5 01:44:24 2022 +0000
feat(measure_theory/measure/finite_measure_weak_convergence): add definition and lemmas of pairing measures with nonnegative continuous test functions. (#9430)
Add definition and lemmas about pairing of `finite_measure`s and `probability_measure`s with nonnegative continuous test functions. These pairings will be used in the definition of the topology of weak convergence (convergence in distribution): the topology will be defined as an induced topology based on them.
Co-authored-by: kkytola <39528102+kkytola@users.noreply.github.com>
commit 5c8243f97bc2ac12f156138d264877d75e1065ee
Author: Eric Wieser <wieser.eric@gmail.com>
Date: Tue Jan 4 23:41:45 2022 +0000
fix(algebra/group/type_tags): resolve an instance diamond caused by over-eager unfolding (#11240)
By setting the `one` and `zero` fields manually, we ensure that they are syntactically equal to the ones found via `has_one` and `has_zero`, rather than potentially having typeclass arguments resolved in a different way.
This seems to fix the failing test.
[Zulip thread](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Diamond.20in.20multiplicative.20nat/near/266824443)
commit 862854edb99451c0cd82ad48abc322b6d011f00f
Author: Yakov Pechersky <ypechersky@treeline.bio>
Date: Tue Jan 4 22:10:13 2022 +0000
chore(ring_theory/localization): fix typo in module docstring (#11245)
There was a mismatch in the module docstring to the decl name later.
commit dc352a643987975c75815a63adb9e6dfe2415ddb
Author: Rob Lewis <Rob.y.lewis@gmail.com>
Date: Tue Jan 4 18:47:59 2022 +0000
chore(.github): include co-author attributions in PR template (#11239)
commit 692b6b7c8ebcfb5aff4cd1a7039d112e33bf46b4
Author: Heather Macbeth <25316162+hrmacbeth@users.noreply.github.com>
Date: Tue Jan 4 18:47:58 2022 +0000
chore(analysis/inner_product_space/basic): adjust decidability assumptions (#11212)
Eliminate the `open_locale classical` in `inner_product_space.basic` and replace by specific decidability assumptions.
commit 49cbce22fae12b2441a4ffacc2d1dbdb65774430
Author: Kyle Miller <kmill31415@gmail.com>
Date: Tue Jan 4 18:47:57 2022 +0000
chore(data/fintype/basic): set.to_finset_univ generalization (#11174)
commit 037147eca296c628b1029963747ffcb3874aeee5
Author: Kexing Ying <kexing.ying19@imperial.ac.uk>
Date: Tue Jan 4 18:47:56 2022 +0000
feat(probability_theory/stopping): define stopped process (#10851)
Co-authored-by: RemyDegenne <Remydegenne@gmail.com>
commit 5df2e7bb77a6e565cbb3ea550d85cd9634a2801c
Author: Eric Wieser <wieser.eric@gmail.com>
Date: Tue Jan 4 16:45:27 2022 +0000
chore(data/polynomial, data/finset/lattice): basic lemmas (#11237)
Co-authored-by: Iván Sadofschi Costa <isadofschi@users.noreply.github.com>
commit 5f3f01f9ce0e993f40131cdf5fefb84340c7799a
Author: Violeta Hernández <vi.hdz.p@gmail.com>
Date: Tue Jan 4 16:45:25 2022 +0000
feat(set_theory/ordinal_arithmetic): Proved `add_log_le_log_mul` (#11228)
That is, `log b u + log b v ≤ log b (u * v)`. The other direction holds only when `b ≠ 2` and `b` is principal multiplicative, and will be added at a much later PR.
commit 18330f63dc0288d4568341754177412f419ba6b7
Author: Mario Carneiro <di.gama@gmail.com>
Date: Tue Jan 4 16:45:24 2022 +0000
feat(tactic/abel): support 0 in group expressions (#11201)
[As reported on Zulip.](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/.60abel.60.20not.20rewriting.20with.20.60sub_zero.60/near/266645648)
fixes #11200
commit b0f2f559c4030caa1b380585197f0bfdf6790afe
Author: Violeta Hernández <vi.hdz.p@gmail.com>
Date: Tue Jan 4 16:45:23 2022 +0000
feat(set_theory/ordinal_arithmetic): Proved `dvd_iff_mod_eq_zero` (#11195)
commit 7f244cfe068bbac2b7c6907073452eac8c8e0f79
Author: Adam Topaz <github@adamtopaz.com>
Date: Tue Jan 4 16:45:22 2022 +0000
feat(category_theory/limits/filtered_colimits_commute_with_finite_limits): A curried variant of the fact that filtered colimits commute with finite limits. (#11154)
commit 06c3ab2b89e1a10420ee3a3bc64be23943e6d1cd
Author: Riccardo Brasca <riccardo.brasca@gmail.com>
Date: Tue Jan 4 16:45:20 2022 +0000
feat(ring_theory/discriminant): add of_power_basis_eq_norm (#11149)
From flt-regular.
commit 4a0e844b90150c47fd792617586ad41b650a7863
Author: Bhavik Mehta <bhavikmehta8@gmail.com>
Date: Tue Jan 4 16:45:19 2022 +0000
feat(data/finset): to_finset empty iff (#11088)
commit 68d2d213b04bd7083020dfea6614292840c0bb9d
Author: Alex J Best <alex.j.best@gmail.com>
Date: Tue Jan 4 16:45:18 2022 +0000
feat(testing/slim_check): teach slim_check about `finsupp`s (#10916)
We add some instances so that `slim_check` can generate `finsupp`s and hence try to provide counterexamples for them.
As the way the original slim_check for functions works is to generate a finite list of random values and pick a default for the rest of the values these `total_functions` are quite close to finsupps already, we just have to map the default value to zero, and prove various things about the support.
There might be conceptually nicer ways of building this instance but this seems functional enough.
Seeing as many finsupp defs are classical (and noncomputable) this isn't quite as useful for generating counterexamples as I originally hoped.
See the test at `test/slim_check.lean` for a basic example of usage
I wrote this while working on flt-regular but it is hopefully useful outside of that
Co-authored-by: Rob Lewis <Rob.y.lewis@gmail.com>
commit 7d42deda9f5bc0d58d746d8f0538557128377559
Author: Yaël Dillies <yael.dillies@gmail.com>
Date: Tue Jan 4 16:45:16 2022 +0000
chore(*): Rename instances (#9200)
Rename
* `lattice_of_linear_order` -> `linear_order.to_lattice`
* `distrib_lattice_of_linear_order` -> `linear_order.to_distrib_lattice`
to follow the naming convention (well, it's currently not explicitly written there, but autogenerated names follow that).
commit b99a98e3ca0eb5c0af9dc14c9fa59d3ec6dd7a32
Author: Eric <37984851+ericrbg@users.noreply.github.com>
Date: Tue Jan 4 15:37:18 2022 +0000
doc(category_theory/limits/shapes/pullbacks): fix doc (#11225)
the link doesn't work with the full stop
commit a30375e0d803c78f8f1f61a8ca0f5945b43518ec
Author: Yury G. Kudryashov <urkud@urkud.name>
Date: Tue Jan 4 13:36:42 2022 +0000
feat(topology/fiber_bundle): a topological fiber bundle is a quotient map (#11194)
* The projection map of a topological fiber bundle (pre)trivialization
is surjective onto its base set.
* The projection map of a topological fiber bundle with a nonempty
fiber is surjective. Since it is also a continuous open map, it is a
quotient map.
* Golf a few proofs.
commit aa82ba00e69064d3446b310810b6b1a0a521eb4f
Author: Yury G. Kudryashov <urkud@urkud.name>
Date: Tue Jan 4 13:36:33 2022 +0000
feat(algebra/opposites): add `add_opposite` (#11080)
Add `add_opposite`, add `to_additive` here and there. More `to_additive` can be added as needed later.
commit a7aa2c874082de938a2afbed70e0741d3b0ce220
Author: Yaël Dillies <yael.dillies@gmail.com>
Date: Tue Jan 4 13:36:24 2022 +0000
feat(data/finset/sigma): A way to lift `finset`-valued functions to a sigma type (#10958)
This defines `finset.sigma_lift : (Π i, α i → β i → finset (γ i)) → Σ i, α i → Σ i, β i → finset (Σ i, γ i)` as the function which returns the finset corresponding to the first coordinate of `a b : Σ i, α i` if they have the same, or the empty set else.
Co-authored-by: Bhavik Mehta <bhavikmehta8@gmail.com>
commit 8bd205985db14dc1f238d6566920d6c01ef34be9
Author: Yaël Dillies <yael.dillies@gmail.com>
Date: Tue Jan 4 13:36:16 2022 +0000
feat(data/finset/slice): `r`-sets and slice (#10685)
Two simple nonetheless useful definitions about set families. A family of `r`-sets is a set of finsets of cardinality `r`. The slice of a set family is its subset of `r`-sets.
commit 1aec9a19b500cc8bcc38df5e141d131d89396d3e
Author: Frédéric Dupuis <dupuisf@iro.umontreal.ca>
Date: Tue Jan 4 12:08:44 2022 +0000
feat(analysis/inner_product_space/dual,adjoint): add some lemmas about extensionality with respect to a basis (#11176)
This PR adds some lemmas about extensionality in inner product spaces with respect to a basis.
commit 03872fdd77e090bb9b609e0b65ed4648d9789403
Author: Andrew Yang <the.erd.one@gmail.com>
Date: Tue Jan 4 09:44:51 2022 +0000
feat(*): Prerequisites for the Spec gamma adjunction (#11209)
Co-authored-by: Junyan Xu <junyanxumath@gmail.com>
commit 9a8e9fa5b9303f03015eff7646b1a9f66f403033
Author: Andrew Yang <the.erd.one@gmail.com>
Date: Tue Jan 4 09:44:50 2022 +0000
chore(category_theory/limits): Generalize universes for `preserves/shapes/pullback.lean` (#10780)
Co-authored-by: Andrew Yang <36414270+erdOne@users.noreply.github.com>
commit 044c1defc8f71c8ac1a8800e59b68603d3b66c8f
Author: Yury G. Kudryashov <urkud@urkud.name>
Date: Tue Jan 4 07:46:59 2022 +0000
feat(analysis/special_functions/trigonometric): a few lemmas (#11217)
Add a few trivial lemmas about `arcsin`/`arccos`.
commit 3045014d8446ea800b9aafb437ff892313080ac0
Author: Yury G. Kudryashov <urkud@urkud.name>
Date: Tue Jan 4 07:46:58 2022 +0000
feat(algebra/order/ring): turn `mul_self_pos` into an `iff` (#11216)
commit 85784b052c795103c833c260a9d712e43ad4be0c
Author: Joseph Myers <jsm@polyomino.org.uk>
Date: Tue Jan 4 07:46:57 2022 +0000
feat(linear_algebra/determinant): `det_units_smul` and `det_is_unit_smul` (#11206)
Add lemmas giving the determinant of a basis constructed with
`units_smul` or `is_unit_smul` with respect to the original basis.
commit 1fc7a93cb224108c99287b41bdb45c87c5b71586
Author: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>
Date: Tue Jan 4 07:46:56 2022 +0000
chore(topology/metric_space/hausdorff_distance): slightly tidy some proofs (#11203)
commit 9d1503a63fb9217f0ff6296d464ff570b26e0630
Author: Sebastian-Monnet <sebastian.monnet@gmail.com>
Date: Tue Jan 4 07:46:55 2022 +0000
feat(field_theory.intermediate_field): add intermediate_field.map_map (#11020)
Co-authored-by: Johan Commelin <johan@commelin.net>
commit 71dc1eab8e279f5100fa841b8472d9d479160a96
Author: Yury G. Kudryashov <urkud@urkud.name>
Date: Tue Jan 4 06:31:42 2022 +0000
feat(topology/maps): preimage of closure/frontier under an open map (#11189)
We had lemmas about `interior`. Add versions about `frontier` and `closure`.
commit 8f391aa552ca7056691e679a6bc016f6fcaee0e2
Author: Heather Macbeth <25316162+hrmacbeth@users.noreply.github.com>
Date: Tue Jan 4 03:53:12 2022 +0000
chore(algebra/module/submodule): switch `subtype_eq_val` to `coe_subtype` (#11210)
Change the name and form of a lemma, from
```lean
lemma subtype_eq_val : ((submodule.subtype p) : p → M) = subtype.val := rfl
```
to
```lean
lemma coe_subtype : ((submodule.subtype p) : p → M) = coe := rfl
```
The latter is the simp-normal form so I claim it should be preferred.
commit 4daaff06058cbee078dc667a2c753c1d33bdc074
Author: Bhavik Mehta <bhavikmehta8@gmail.com>
Date: Tue Jan 4 01:48:54 2022 +0000
feat(data/nat/prime): factors sublist of product (#11104)
This PR changes the existing `factors_subset_right` to give a stronger sublist conclusion (which trivially can be used to reproduce the subst version).
commit 62d814a4f9f6fa650ce0598e02dcd3a018a0796f
Author: Yaël Dillies <yael.dillies@gmail.com>
Date: Mon Jan 3 20:30:05 2022 +0000
refactor(order/lexicographic): Change the `lex` synonym (#10926)
At least five types have a natural lexicographic order, namely:
* `α ⊕ β` where everything on the left is smaller than everything on the right
* `Σ i, α i` where things are first ordered following `ι`, then following `α i`
* `Σ' i, α i` where things are first ordered following `ι`, then following `α i`
* `α × β` where things are first ordered following `α`, then following `β`
* `finset α`, which is in a specific sene the dual of `finset.colex`.
And we could even add `Π i, α i`, `ι →₀ α`, `Π₀ i, α i`, etc... although those haven't come up yet in practice.
Hence, we generalize the `lex` synonym away from `prod` to make it a general purpose synonym to equip a type with its lexicographical order. What was `lex α β` now is `α ×ₗ β`.
Note that this PR doesn't add any of the aforementioned instances.
commit 9d0fd52315f399d390b2d5a727972cb551c0a16f
Author: Rémy Degenne <Remydegenne@gmail.com>
Date: Mon Jan 3 18:55:41 2022 +0000
feat(measure_theory/function/lp_space): use has_measurable_add2 instead of second_countable_topology (#11202)
Use the weaker assumption `[has_measurable_add₂ E]` instead of `[second_countable_topology E]` in 4 lemmas.
commit 724989582f9efd7210e4abd56da4b12aac3095cb
Author: Joseph Myers <jsm@polyomino.org.uk>
Date: Mon Jan 3 16:25:35 2022 +0000
feat(analysis/inner_product_space/basic): negating orthonormal vectors (#11208)
Add a lemma that, given an orthonormal family, negating some of the
vectors in it produces another orthonormal family.
commit 83f40364c6329eb42bcb659f53a6e803004f0133
Author: Eric <ericrboidi@gmail.com>
Date: Mon Jan 3 15:26:28 2022 +0000
feat(*/cyclotomic): update is_root_cyclotomic_iff to use ne_zero (#11071)
Co-authored-by: Johan Commelin <johan@commelin.net>
commit 236d978daf8ce20b0d7bad7a4a60985b65f0f04d
Author: Joseph Myers <jsm@polyomino.org.uk>
Date: Mon Jan 3 14:30:17 2022 +0000
feat(linear_algebra/matrix/basis): `to_matrix_units_smul` and `to_matrix_is_unit_smul` (#11191)
Add lemmas that applying `to_matrix` to a basis constructed with
`units_smul` or `is_unit_smul` produces the corresponding diagonal
matrix.
commit 4b3198b9453e8b09da042eea0d872dfd0d3dbea2
Author: tb65536 <tb65536@uw.edu>
Date: Mon Jan 3 12:49:02 2022 +0000
feat(combinatorics/configuration): `has_lines` implies `has_points`, and vice versa (#11170)
If `|P| = |L|`, then `has_lines` and `has_points` are equivalent!
commit a10cb2f395b8d002cfca01aca3a98a5736e28006
Author: Stuart Presnell <stuart.presnell@gmail.com>
Date: Mon Jan 3 11:27:40 2022 +0000
feat(algebra/big_operators/associated): `dvd_prod_iff` for `finset` and `finsupp` (#10675)
Adding the counterparts of `dvd_prod_iff` (in #10624) for `finset` and `finsupp`.
commit a813cf5c732ac4cc2d7b430e6ff733c68a451655
Author: Jireh Loreaux <loreaujy@gmail.com>
Date: Mon Jan 3 10:32:11 2022 +0000
chore(algebra/algebra/spectrum): move `exists_spectrum_of_is_alg_closed_of_finite_dimensional` (#10919)
Move a lemma from `field_theory/is_alg_closed/basic` into `algebra/algebra/spectrum` which belongs in this relatively new file. Also, rename (now in `spectrum` namespace) and refactor it slightly; and update the two references to it accordingly.
- [x] depends on: #10783
Co-authored-by: Vierkantor <vierkantor@vierkantor.com>
commit 49bf3d3ef8dae581bf25f207c07092c9a7597cdb
Author: Yakov Pechersky <ffxen158@gmail.com>
Date: Mon Jan 3 07:35:22 2022 +0000
feat(data/polynomial/taylor): taylor_mul (#11193)
Co-authored-by: Johan Commelin <johan@commelin.net>
commit a49ee49b4bfa72c04c3db02288e420a21dae0692
Author: Yaël Dillies <yael.dillies@gmail.com>
Date: Mon Jan 3 07:35:21 2022 +0000
feat(data/finset/functor): Functor structures for `finset` (#10980)
This defines the monad, the commutative applicative and the (almost) traversable functor structures on `finset`.
It all goes in a new file `data.finset.functor` and picks up the `functor` instance that was stranded in `data.finset.basic` by Scott in #2997.
commit 138c61fce58aef579c1bc052066a9a5829774583
Author: Yakov Pechersky <ffxen158@gmail.com>
Date: Mon Jan 3 06:54:39 2022 +0000
chore(field_theory/ratfunc): comm_ring (ratfunc K) (#11188)
Previously, the file only gave a `field (ratfunc K)` instance,
requiring `comm_ring K` and `is_domain K`.
In fact, `ratfunc K` is a `comm_ring` regardless of the `is_domain`.
The upstream instance is proven first, with a generalized tactic.
commit 03a54829aed1f79e696b7a3b1847fcc521de6398
Author: Yury G. Kudryashov <urkud@urkud.name>
Date: Sun Jan 2 23:55:46 2022 +0000
chore(topology/continuous_on): fix a typo (#11190)
`eventually_nhds_with_of_forall` → `eventually_nhds_within_of_forall`
commit 3f7776136e1bf0310cb01c299d23b106ef2e2016
Author: Yakov Pechersky <ffxen158@gmail.com>
Date: Sun Jan 2 17:21:44 2022 +0000
feat(ring_theory/algebraic): algebraic functions (#11156)
Accessible via a new `algebra (polynomial R) (R → R)`
and a generalization that gives `algebra (polynomial R) (S → S)` when `[algebra R S]`.
commit ebdbe6b00344560e39edec913f63ddb1f6546bdf
Author: Yury G. Kudryashov <urkud@urkud.name>
Date: Sat Jan 1 20:23:07 2022 +0000
feat(topology/algebra/ordered): new lemmas, update (#11184)
* In `exists_seq_strict_mono_tendsto'` and `exists_seq_strict_anti_tendsto'`, prove that `u n` belongs to the corresponding open interval.
* Add `exists_seq_strict_anti_strict_mono_tendsto`.
* Rename `is_lub_of_tendsto` to `is_lub_of_tendsto_at_top`, rename `is_glb_of_tendsto` to `is_glb_of_tendsto_at_bot`.
* Add `is_lub_of_tendsto_at_bot`, `is_glb_of_tendsto_at_top`.
commit 02d02dfc2767d5211f58d4d7e8e426dc63a21de4
Author: Yury G. Kudryashov <urkud@urkud.name>
Date: Sat Jan 1 19:07:15 2022 +0000
chore(measure_theory): fix TC assumptions in 2 lemmas (#11185)
With new assumptions, these lemmas work, e.g., for `β = ι → ℝ`.
commit c1b1041703932ae68c5622e33ef97399d6e94e2d
Author: Yury G. Kudryashov <urkud@urkud.name>
Date: Sat Jan 1 19:07:13 2022 +0000
feat(topology/metric_space/basic): add `fin.dist_insert_nth_insert_nth` (#11183)
commit 6486e9b34092e78f876619038814d3a7fb58fb77
Author: Violeta Hernández <vi.hdz.p@gmail.com>
Date: Sat Jan 1 17:09:52 2022 +0000
chore(order/rel_classes): Removed unnecessary `classical` (#11180)
Not sure what that was doing here.
commit 93cf56c59ad9645fc79d7d8caa37f185e8bad7ff
Author: Andrew Yang <the.erd.one@gmail.com>
Date: Sat Jan 1 15:44:59 2022 +0000
feat(algebraic_geometry/*): The map `F.stalk y ⟶ F.stalk x` for `x ⤳ y` (#11144)
Co-authored-by: Andrew Yang <36414270+erdOne@users.noreply.github.com>
commit 892d465a22dbaa12fa7003cc732fb27ba4a4dbee
Author: Oliver Nash <github@olivernash.org>
Date: Sat Jan 1 14:44:14 2022 +0000
feat(linear_algebra/multilinear/basic): the space of multilinear maps is finite-dimensional when the components are finite-dimensional (#10504)
Formalized as part of the Sphere Eversion project.
commit 53533697265b23a58f41816a841b23083db915a7
Author: tb65536 <tb65536@uw.edu>
Date: Sat Jan 1 13:55:32 2022 +0000
feat(combinatorics/configuration): Line count equals point count (#11169)
In a configuration satisfying `has_lines` or `has_points`, if the number of points equals the number of lines, then the number of lines through a given point equals the number of points on a given line.
commit a6c82afb13e6ba417985e238f845d3d65f72e32f
Author: Julian-Kuelshammer <julian.kuelshammer@math.uu.se>
Date: Sat Jan 1 13:55:31 2022 +0000
feat(group_theory/specific_groups/*): computes the exponents of the dihedral and generalised quaternion groups (#11166)
This PR shows that the exponent of the dihedral group of order `2n` is equal to `lcm n 2` and that the exponent of the generalised quaternion group of order `4n` is `2 * lcm n 2`
Co-authored-by: Eric Rodriguez <ericrboidi@gmail.com>
Co-authored-by: Julian-Kuelshammer <68201724+Julian-Kuelshammer@users.noreply.github.com>
commit ad76a5eee59757353c583279570b4801ed43ee4e
Author: Yakov Pechersky <ffxen158@gmail.com>
Date: Sat Jan 1 13:55:30 2022 +0000
feat(data/nat/log): log_mul, log_div (#11164)
Even with division over natural, the log "spec" holds.
Co-authored-by: Yakov Pechersky <pechersky@users.noreply.github.com>
commit 23b01cc447875bb7e8604fc18408108db9fb0454
Author: Andrew Yang <the.erd.one@gmail.com>
Date: Sat Jan 1 11:59:04 2022 +0000
feat(algebraic_geometry): The function field of an integral scheme (#11147)
Co-authored-by: Andrew Yang <36414270+erdOne@users.noreply.github.com>
commit 1594b0ca22ea5041befb6a62bdd266d1a6cd471b
Author: Heather Macbeth <25316162+hrmacbeth@users.noreply.github.com>
Date: Sat Jan 1 02:32:45 2022 +0000
feat(normed_space/lp_space): Lp space for `Π i, E i` (#11015)
For a family `Π i, E i` of normed spaces, define the subgroup with finite lp norm, and prove it is a `normed_group`. Many parts adapted from the development of `measure_theory.Lp` by @RemyDegenne.
https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Lp.20space
commit 742ec88c19df53531dc6f0f690bcd1ac6cec22a8
Author: Yury G. Kudryashov <urkud@urkud.name>
Date: Sat Jan 1 00:20:37 2022 +0000
feat(data/set/*): lemmas about `monotone`/`antitone` and sets/intervals (#11173)
* Rename `set.monotone_inter` and `set.monotone_union` to
`monotone.inter` and `monotone.union`.
* Add `antitone` versions of some `monotone` lemmas.
* Specialize `Union_Inter_of_monotone` for `set.pi`.
* Add lemmas about `⋃ x, Ioi (f x)`, `⋃ x, Iio (f x)`, and `⋃ x, Ioo (f x) (g x)`.
* Add dot notation lemmas `monotone.Ixx` and `antitone.Ixx`.
commit 979f2e729f58892a232d4ec8696bc23f655457c7
Author: Kevin Buzzard <k.buzzard@imperial.ac.uk>
Date: Sat Jan 1 00:20:36 2022 +0000
fix(order/filter/ultrafilter): dedup instance names (#11171)
commit da54388a50b504a5f2e8f25bdf991a737e818624
Author: agusakov <agusakov@udel.edu>
Date: Sat Jan 1 00:20:35 2022 +0000
feat(combinatorics/simple_graph/srg): is_SRG_with for complete graphs, edgeless graphs, and complements (#5698)
We add the definition of a strongly regular graph and prove some useful lemmas about them.
Co-authored-by: agusakov <39916842+agusakov@users.noreply.github.com>
commit 8db2fa05bdcfed5d6db0c4ce9ece038a9904c868
Author: David Wärn <codwarn@gmail.com>
Date: Fri Dec 31 22:23:24 2021 +0000
chore(category_theory/closed/cartesian): make exp right-associative (#11172)
This makes `X ⟹ Y ⟹ Z` parse as `X ⟹ (Y ⟹ Z)`, like ordinary function types.
commit 559951cd0e861fe41629d4e93ecef11cffb6502d
Author: prakol16 <praneeth.kolichala@gmail.com>
Date: Fri Dec 31 22:23:23 2021 +0000
feat(data/quot): Add quotient pi induction (#11137)
I am planning to use this later to show that the (pi) product of homotopy classes of paths is well-defined, and prove
properties about that product.
Co-authored-by: prakol16 <prakol16@users.noreply.github.com>
commit 200f47d36636dc4cd0b0d9e4ee358da533531702
Author: Jireh Loreaux <loreaujy@gmail.com>
Date: Fri Dec 31 22:23:22 2021 +0000
feat(analysis/normed_space/banach_steinhaus): prove the standard Banach-Steinhaus theorem (#10663)
Here we prove the Banach-Steinhaus theorem for maps from a Banach space into a (semi-)normed space. This is the standard version of the theorem and the proof proceeds via the Baire category theorem. Notably, the version from barelled spaces to locally convex spaces is not included because these spaces do not yet exist in `mathlib`. In addition, it is established that the pointwise limit of continuous linear maps from a Banach space into a normed space is itself a continuous linear map.
- [x] depends on: #10700
Co-authored-by: Patrick Massot <patrickmassot@free.fr>
commit ea710ca6ceaac4a1398e7ee87f32d5cb83f8c482
Author: Yakov Pechersky <ffxen158@gmail.com>
Date: Fri Dec 31 21:03:20 2021 +0000
feat(data/polynomial/ring_division): golf and generalize `leading_coeff_div_by_monic_of_monic` (#11077)
No longer require that the underlying ring is a domain.
Also added helper API lemma `leading_coeff_monic_mul`.
commit 8ec59f9c837efd0cb51be291c163ce311722285f
Author: Stuart Presnell <stuart.presnell@gmail.com>
Date: Fri Dec 31 21:03:19 2021 +0000
feat(data/int/gcd): add theorem `gcd_least_linear` (#10743)
For nonzero integers `a` and `b`, `gcd a b` is the smallest positive integer that can be written in the form `a * x + b * y` for some pair of integers `x` and `y`
This is an extension of Bézout's lemma (`gcd_eq_gcd_ab`), which says that `gcd a b` can be written in that form.
commit e4607f8f819db97e16e900cf5c38b7d5914cbea4
Author: Eric Wieser <wieser.eric@gmail.com>
Date: Fri Dec 31 19:13:58 2021 +0000
chore(data/sym/basic): golf and add missing simp lemmas (#11160)
By changing `cons` to not use pattern matching, `(a :: s).1 = a ::ₘ s.1` is true by `rfl`, which is convenient here and there for golfing.
commit fbbbdfa0a0f3ebdc37025908fc3be1604ed174a9
Author: Frédéric Dupuis <dupuisf@iro.umontreal.ca>
Date: Fri Dec 31 19:13:57 2021 +0000
feat(algebra/star/self_adjoint): define the self-adjoint elements of a star additive group (#11135)
Given a type `R` with `[add_group R] [star_add_monoid R]`, we define `self_adjoint R` as the additive subgroup of self-adjoint elements, i.e. those such that `star x = x`. To avoid confusion, we move `is_self_adjoint` (which defines this to mean `⟪T x, y⟫ = ⟪x, T y⟫` in an inner product space) to the `inner_product_space` namespace.
commit fdf09df0ba410ac68ed716ab4cdfcce26559209b
Author: Yakov Pechersky <ffxen158@gmail.com>
Date: Fri Dec 31 19:13:55 2021 +0000
feat(data/polynomial/degree/lemmas): (nat_)degree_sum_eq_of_disjoint (#11121)
Also two helper lemmas on `nat_degree`.
Generalize `degree_sum_fin_lt` to semirings
commit c4caf0ee72988fde59158b189a539c7c517c6b4e
Author: Oliver Nash <github@olivernash.org>
Date: Fri Dec 31 16:13:18 2021 +0000
feat(linear_algebra/multilinear/basic): add dependent version of `multilinear_map.dom_dom_congr_linear_equiv` (#10474)
Formalized as part of the Sphere Eversion project.
commit 9a38c196381a86501e53c6e6b92a8a7682a0418a
Author: Yakov Pechersky <ffxen158@gmail.com>
Date: Fri Dec 31 14:15:50 2021 +0000
feat(data/list/indexes): map_with_index_eq_of_fn (#11163)
Some `list.map_with_index` API.
commit b92afc9007b533272087efd567ba8e480e9d9e37
Author: Eric Wieser <wieser.eric@gmail.com>
Date: Fri Dec 31 14:15:49 2021 +0000
chore(data/equiv/basic): missing dsimp lemmas (#11159)
commit bcf1d2ddd047fcba2f641d5bf4bf86e0eba896a6
Author: Adam Topaz <github@adamtopaz.com>
Date: Fri Dec 31 14:15:48 2021 +0000
feat(category_theory/sites/plus): Adds a functorial version of `J.diagram P`, functorial in `P`. (#11155)
commit 7b387924a1845ea8a590ae8d4e5eaee6e8089d99
Author: Adam Topaz <github@adamtopaz.com>
Date: Fri Dec 31 14:15:46 2021 +0000
feat(category_theory/limits/functor_category): Some additional isomorphisms involving (co)limits of functors. (#11152)
commit b142b6979c68e5df20ec3628b93c44668ef74310
Author: Stuart Presnell <stuart.presnell@gmail.com>
Date: Fri Dec 31 14:15:45 2021 +0000
feat(data/list/count): add lemma `count_le_count_map` (#11148)
Generalises `count_map_map`: for any `f : α → β` (not necessarily injective), `count x l ≤ count (f x) (map f l)`
commit dc57b5449561eb76d8af6862f8eb86a422cd0cd0
Author: Andrew Yang <the.erd.one@gmail.com>
Date: Fri Dec 31 14:15:44 2021 +0000
feat(ring_theory/localization): Transferring `is_localization` along equivs. (#11146)
Co-authored-by: Andrew Yang <36414270+erdOne@users.noreply.github.com>
commit bc5e00813ef5e16eaa17c70683d512228bf1907b
Author: Yaël Dillies <yael.dillies@gmail.com>
Date: Fri Dec 31 14:15:43 2021 +0000
feat(data/dfinsupp/order): Pointwise order on finitely supported dependent functions (#11138)
This defines the pointwise order on `Π₀ i, α i`, in very much the same way as in `data.finsupp.order`. It also moves `data.dfinsupp` to `data.dfinsupp.basic`.
commit 2e8ebdc083b8eaf48d068447e0cffcb0201c936d
Author: Joël Riou <joel.riou@universite-paris-saclay.fr>
Date: Fri Dec 31 14:15:42 2021 +0000
feat(algebra/homology): Construction of null homotopic chain complex … (#11125)
…morphisms and one lemma on addivity of homotopies
Co-authored-by: Joël Riou <37772949+joelriou@users.noreply.github.com>
commit ff7e837a7487581042834f5101fdcd05c434fa37
Author: tb65536 <tb65536@uw.edu>
Date: Fri Dec 31 14:15:41 2021 +0000
feat(combinatorics/configuration): Variant of `exists_injective_of_card_le` (#11116)
Proves a variant of `exists_injective_of_card_le` that will be useful in an upcoming proof.
commit 1fd70b1b8b33840d1b1ba7ac1851aa3a1e8841bf
Author: tb65536 <tb65536@uw.edu>
Date: Fri Dec 31 14:15:41 2021 +0000
refactor(algebra/big_operators/basic): Reorder lemmas (#11113)
This PR does the following things:
- Move `prod_bij` and `prod_bij'` earlier in the file, so that they can be put to use.
- Move `prod_product` and `prod_product'` past `prod_sigma` and `prod_sigma'` down to `prod_product_right` and `prod_product_right'`.
- Use `prod_bij` and `prod_sigma` to give an easier proof of `prod_product`.
- The new proof introduces `prod_finset_product` and the remaining three analogs of the four `prod_product` lemmas.
`prod_finset_product` is a lemma that I found helpful in my own work.
commit 99e3ffbd3e732d466312bb0680e6ce5140a5bbbc
Author: Rob Lewis <Rob.y.lewis@gmail.com>
Date: Fri Dec 31 14:15:40 2021 +0000
feat(data/fin/tuple): new directory and file on sorting (#11096)
Code written by @kmill at https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there.20code.20for.20X.3F/topic/Permutation.20to.20make.20a.20function.20monotone
Co-authored by: Kyle Miller <kmill31415@gmail.com>
Co-authored-by: Rob Lewis <rob.y.lewis@gmail.com>
commit 06a019715809b7c4c67fbf550578a2ea9d55c13e
Author: Yuma Mizuno <mizuno.y.aj@gmail.com>
Date: Fri Dec 31 14:15:39 2021 +0000
feat(category_theory/bicategory/basic): define bicategories (#11079)
This PR defines bicategories and gives basic lemmas.
commit a5573f375bd8dc13cf2ebdb1b02d9cbf85b0a9c7
Author: Alex J Best <alex.j.best@gmail.com>
Date: Fri Dec 31 14:15:37 2021 +0000
feat(data/{fin,multi}set/powerset): add some lemmas about powerset_len (#10866)
For both multisets and finsets
From flt-regular
commit 78a9900b40942b6b1181ef21dc31be8f24473eeb
Author: Christopher Hoskin <christopher.hoskin@gmail.com>
Date: Fri Dec 31 12:26:01 2021 +0000
refactor(algebra/group/hom_instances): relax semiring to non_unital_non_assoc_semiring in add_monoid_hom.mul (#11165)
Previously `algebra.group.hom_instances` ended with some results showing that left and right multiplication operators are additive monoid homomorphisms between (unital, associative) semirings. The assumptions of a unit and associativity are not required for these results to work, so we relax the condition to `non_unital_non_assoc_semiring`.
Required for #11073 .
commit dc1525fb3ef6eb4348fb1749c302d8abc303d34a
Author: Yaël Dillies <yael.dillies@gmail.com>
Date: Fri Dec 31 07:44:08 2021 +0000
docs(data/sum/basic): Expand module docstring and cleanup (#11158)
This moves…
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.
Adding the counterparts of
dvd_prod_iff(in #10624) forfinsetandfinsupp.