Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

[Merged by Bors] - feat(group_theory/noncomm_pi_coprod): homomorphism from pi monoids or groups #11744

Closed
wants to merge 148 commits into from
Closed

[Merged by Bors] - feat(group_theory/noncomm_pi_coprod): homomorphism from pi monoids or groups #11744

Show file tree
Hide file tree
Changes from 44 commits
Commits
Show all changes
148 commits
Select commit Hold shift + click to select a range
8895dd8
first stab at hom out of pi group
nomeata Jan 31, 2022
47cf2cd
Please lint a bit
nomeata Jan 31, 2022
637058f
time flies
nomeata Jan 31, 2022
363f6ff
shuffling whitespace
nomeata Jan 31, 2022
204dea2
Get rid of ugly have
nomeata Jan 31, 2022
e42f4aa
Base development on noncomm_prod
nomeata Jan 31, 2022
2aef604
Redundant [decidable_eq I]
nomeata Jan 31, 2022
7e18e9b
Specialize the theorem to normal subgroups and subgroup inclusion
nomeata Jan 31, 2022
cda4df8
feat(group_theory/subgroup/basic): add commute_of_normal_of_disjoint
nomeata Jan 31, 2022
945d984
Stash coprimality argument
nomeata Jan 31, 2022
80ef71c
Merge remote-tracking branch 'origin/joachim/commute_of_normal' into …
nomeata Jan 31, 2022
723e30a
Injectivity via coprimality of groups. More suited for sylow group.
nomeata Jan 31, 2022
88398c2
Big clean-up and documentation
nomeata Feb 1, 2022
ba94eeb
Prune imports
nomeata Feb 1, 2022
9d87cf4
Remove kinda unused lemma
nomeata Feb 1, 2022
29f828a
whitespace
nomeata Feb 1, 2022
05e4029
Ups
nomeata Feb 1, 2022
e73b58c
Make it lint-clean
nomeata Feb 1, 2022
fdda033
Less underscores
nomeata Feb 1, 2022
4d6d5be
erge branch 'master' of github.com:leanprover-community/mathlib into …
nomeata Feb 1, 2022
4b7f97f
Update src/group_theory/pi_hom.lean
nomeata Feb 9, 2022
d576d7c
Proof cosmetics
nomeata Feb 10, 2022
3cdf4b9
Move order of inv
nomeata Feb 10, 2022
d33876f
Apply suggestions from code review
nomeata Feb 11, 2022
9de2537
Merge branch 'master' of github.com:leanprover-community/mathlib into…
nomeata Feb 11, 2022
f56d66d
Use monoid_hom.single, not function.update
nomeata Feb 11, 2022
e810447
simplify independence proof and remove lemmas
alreadydone Feb 12, 2022
7cc8b50
Define hom for monoids
nomeata Feb 12, 2022
e1257d0
Apply suggestions from code review
nomeata Feb 12, 2022
194253f
polish proof
alreadydone Feb 12, 2022
50712bb
Don’t use fact nor parameters
nomeata Feb 14, 2022
8da6ad5
Avoid simp followed by tauto
nomeata Feb 14, 2022
dfcc956
Update src/group_theory/pi_hom.lean
nomeata Feb 14, 2022
dfccab3
Say monoid_hom.noncomm_pi_coprod
nomeata Feb 15, 2022
81ecc8c
Add to_additive
nomeata Feb 15, 2022
e5c3a97
Update src/group_theory/order_of_element.lean
nomeata Feb 15, 2022
f0d5a5c
Use order_of_map_dvd
nomeata Feb 15, 2022
62da911
Additive docstrings
nomeata Feb 16, 2022
ac06e68
s/I/ι/g
nomeata Feb 16, 2022
1cf2f74
Fix typo in filename
nomeata Feb 16, 2022
161d1a3
Fix very embarrasing search-and-replace mistake
nomeata Feb 16, 2022
858a150
Refine some lemma names
nomeata Feb 17, 2022
fd01d65
Avoid open_locale classical
nomeata Feb 21, 2022
45da268
More pleasing classical linter
nomeata Feb 21, 2022
a22e26b
Move coprime_prod_left to src/data/nat/gcd.lean
nomeata Feb 24, 2022
ceccaf7
feat(data/nat/gcd): add coprime_prod_left and coprime_prod_right
nomeata Feb 24, 2022
823a972
Merge branch 'joachim/coprie_prod_left' into joachim/pi_nom
nomeata Feb 24, 2022
b477bd1
s/in_sup/mem_bsupr/g
nomeata Feb 24, 2022
61fdbfc
Review comments
nomeata Feb 24, 2022
06e42bb
Add universal property
nomeata Feb 24, 2022
02bf466
More exploration
nomeata Feb 24, 2022
ce1e1c1
kill sorries
alreadydone Feb 25, 2022
3bf0e6f
Classical linter
nomeata Feb 25, 2022
7e7dc82
Generalize a bit
nomeata Feb 25, 2022
69d481b
Simplify
nomeata Feb 25, 2022
d90d987
Move lemmas
nomeata Feb 25, 2022
4216e43
feat(data/list/prod_monoid): finite pi lemmas
nomeata Feb 25, 2022
ebcdc9a
Merge branch 'joachim/finite_pi_ext' into joachim/pi_nom
nomeata Feb 25, 2022
53f4397
Update src/data/finset/noncomm_prod.lean
nomeata Feb 25, 2022
6930f46
Don’ use monoid_hom.single_commute
nomeata Feb 26, 2022
c7a6873
Rename to prod_le_pow_of_forall_le
nomeata Feb 26, 2022
ab6bf7d
Docstring
nomeata Feb 26, 2022
b0b7179
Remove monoid_hom.single_commute
nomeata Feb 26, 2022
817f556
Generalize noncomm_prod_map and its dependencies
nomeata Feb 26, 2022
5ae1527
Line length
nomeata Feb 26, 2022
98fbc91
Fix fallout
nomeata Feb 27, 2022
ab10503
Merge branch 'joachim/finite_pi_ext' into joachim/pi_nom
nomeata Feb 27, 2022
5eaff25
More juggling of variables
nomeata Feb 27, 2022
d153089
Fix more fallout
nomeata Feb 27, 2022
d6abc52
Merge branch 'joachim/finite_pi_ext' into joachim/pi_nom
nomeata Feb 27, 2022
19035bb
More monoid_hom_class fallout
nomeata Feb 27, 2022
699653c
More monoid_hom_class fallout
nomeata Feb 27, 2022
6f1b066
More monoid_hom_class fallout
nomeata Feb 27, 2022
5981a05
Undo changing `map_list_prod` to `monoid_hom_class`
nomeata Feb 27, 2022
177a8d7
Add docstrings
nomeata Mar 3, 2022
45c6798
Merge remote-tracking branch 'origin/master' into joachim/finite_pi_ext
eric-wieser Mar 5, 2022
507d099
Merge commit 'e96cf5e693dc14935c2cca01b091c09fd4bcc786' into joachim/…
nomeata Mar 5, 2022
f6304b2
Merge branch 'joachim/finite_pi_ext' into joachim/pi_nom
nomeata Mar 5, 2022
6b0dcba
Merge branch 'joachim/coprie_prod_left' into joachim/pi_nom
nomeata Mar 5, 2022
fa6ce2e
Apply code review
nomeata Mar 5, 2022
72e3168
Apply more code review
nomeata Mar 5, 2022
cfd84be
Phrase lemmas wrt. pi.mul_single
nomeata Mar 5, 2022
fc18403
Merge branch 'joachim/finite_pi_ext' into joachim/pi_nom
nomeata Mar 5, 2022
137fb1b
Fix apply-lemmas for monoid_hom.single
nomeata Mar 5, 2022
5d9945c
Stick closer to pi.mul_single
nomeata Mar 5, 2022
0b30fdc
Fix apply-lemmas for monoid_hom.single
nomeata Mar 5, 2022
4e12c99
Merge branch 'joachim/finite_pi_ext' into joachim/pi_nom
nomeata Mar 5, 2022
88710b8
Fix fallout
nomeata Mar 5, 2022
4cdd571
Merge branch 'joachim/finite_pi_ext' into joachim/pi_nom
nomeata Mar 5, 2022
799a4ef
Throw in some to_additive attributes
nomeata Mar 5, 2022
aa37048
lint
nomeata Mar 5, 2022
0f37afe
feat(data/list/prod_monoid): add prod_eq_pow_of_forall_eq
nomeata Mar 6, 2022
47542b6
fix(src/algebra/group/pi): Fix apply-simp-lemmas for monoid_hom.single
nomeata Mar 6, 2022
cbad437
lint
nomeata Mar 5, 2022
59e7029
Merge branch 'joachim/single-simp-normal' into joachim/finite_pi_ext
nomeata Mar 6, 2022
cec535a
Merge branch 'joachim/prod_eq_pow_of_forall_eq' into joachim/finite_p…
nomeata Mar 6, 2022
2905a60
Use npow, not pow, in name, so that to_additive does the right thing
nomeata Mar 6, 2022
73a9e24
Rename le_prod_of_forall_le to npow_le_prod_of_forall_le
nomeata Mar 6, 2022
c242aaa
Use `∀ (x ∈ l),` syntax
nomeata Mar 6, 2022
95b0ec9
Try to teach to_additive about `pow` naming convention
nomeata Mar 6, 2022
5d4660b
Explicit name to avoid name clashes
nomeata Mar 6, 2022
10fdc85
More names are correct now
nomeata Mar 6, 2022
c2d6dde
Even more names are correct now
nomeata Mar 6, 2022
30ca722
Even more names are correct now (order_of_element)
nomeata Mar 6, 2022
ca6c531
Even more names are correct now (exponent.lean)
nomeata Mar 6, 2022
b076f28
Even more names are correct now (topology/continuous_function/algebra…
nomeata Mar 6, 2022
b589335
Say pow, not npow
nomeata Mar 6, 2022
8479435
Merge commit '28c902d86d7904b662d6caf6c9b211b05c485728' into joachim/…
nomeata Mar 6, 2022
921fcc3
Merge branch 'joachim/single-simp-normal' into joachim/finite_pi_ext
nomeata Mar 6, 2022
65c37ca
Fix sum_divisors_prime_pow
nomeata Mar 6, 2022
6123b28
More correct names
nomeata Mar 6, 2022
98184e3
Merge branch 'joachim/to_additive_pow' into joachim/prod_eq_pow_of_fo…
nomeata Mar 7, 2022
cdd20f6
Merge commit 'eb46e7e3cf98edd45bd1cce2227edb90d7e4426d' into joachim/…
nomeata Mar 7, 2022
fcc05b5
Merge branch 'joachim/to_additive_pow' into joachim/prod_eq_pow_of_fo…
nomeata Mar 7, 2022
10c68ec
Merge branch 'joachim/prod_eq_pow_of_forall_eq' into joachim/finite_p…
nomeata Mar 7, 2022
27d120f
Merge branch 'joachim/finite_pi_ext' into joachim/pi_nom
nomeata Mar 7, 2022
48f3938
Big refactoring, more lemmas about noncomm_prod, no more noncomm_pi_c…
nomeata Mar 7, 2022
9a82371
supr_le, not bsupr_le!
nomeata Mar 7, 2022
40276be
Weaken lemma
nomeata Mar 7, 2022
923f7f8
Make lint a bit happy
nomeata Mar 7, 2022
4066009
Reorder some hypotheses
nomeata Mar 7, 2022
c9932f3
Moving some lemmas
nomeata Mar 7, 2022
4e78f24
Rename lemma
nomeata Mar 7, 2022
06a48a1
feat(group_theory/subgroup/basic): disjoint_iff_mul_eq_one
nomeata Mar 7, 2022
048a979
feat(data/finset/noncomm_prod): assorted lemmas
nomeata Mar 7, 2022
cf88139
Merge branch 'joachim/noncomm_prod_lemmas' into joachim/pi_nom
nomeata Mar 7, 2022
96db2d5
Update src/data/finset/noncomm_prod.lean
nomeata Mar 7, 2022
d0ae33f
Merge branch 'joachim/noncomm_prod_lemmas' into joachim/pi_nom
nomeata Mar 7, 2022
15d7b4a
Fix merge mistake
nomeata Mar 7, 2022
e6f2b3b
Avoid the need for finset.noncomm_prod_congr
nomeata Mar 8, 2022
8f678af
Simplify further
nomeata Mar 8, 2022
933682c
Merge remote-tracking branch 'origin/master' into joachim/prod_eq_pow…
nomeata Mar 11, 2022
b4c4c3a
Undo renaming, now happening in #12589
nomeata Mar 11, 2022
c5dd22f
Rename the new lemma
nomeata Mar 11, 2022
a31fe5d
Merge commit 'e3ad468bb46b2773596ec7329c4a298d71a1df08' into joachim/…
nomeata Mar 11, 2022
e0e414f
Merge branch 'joachim/prod_eq_pow_of_forall_eq' into joachim/finite_p…
nomeata Mar 11, 2022
bad3bfe
Merge branch 'master' of github.com:leanprover-community/mathlib into…
nomeata Mar 11, 2022
804d7d8
Rename lemmas according to latest fashion
nomeata Mar 11, 2022
d80f844
Multisetify noncomm_prod_map
nomeata Mar 12, 2022
4961f66
Multisetify noncomm_prod_eq_pow_card
nomeata Mar 12, 2022
ab6f639
Golf
nomeata Mar 12, 2022
700f309
Avoid rather specialized lemma
nomeata Mar 12, 2022
92719f4
Use pi.mul_single_apply_commute
nomeata Mar 12, 2022
bf98c60
Apply suggestions from code review
nomeata Mar 14, 2022
4ce80a6
Merge commit 'refs/pull/12291/head' of github.com:leanprover-communit…
nomeata Mar 14, 2022
3bf4c4b
Merge commit '09ea7fb00a1154b17423e8285313c61e7c427ad7' into joachim/…
nomeata Mar 14, 2022
9206f90
Post-merge update
nomeata Mar 14, 2022
9197315
fix partly embarrassing typos
nomeata Mar 15, 2022
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Jump to
Jump to file
Failed to load files.
Diff view
Diff view