leanprover-community/mathlib

Pull Requests Commits
merge
kim-em committed 3 years ago
507e1652
feat(data/(d)finsupp): well-foundedness of lexicographic and product orders (#16772)
alreadydone committed 3 years ago
e9b8651e
initial split
kim-em committed 3 years ago
7533e6fe
add downstream imports
kim-em committed 3 years ago
a5c37779
chore(data/polynomial/degree): golf a proof (#17322)
urkud committed 3 years ago
59386b20
feat(combinatorics/simple_graph/connectivity): `is_bridge` and cycle characterization (#17306)
kmill committed 3 years ago
d3abacf0
chore(algebra/ne_zero): move the dependencies out (#17177)
digama0 committed 3 years ago
9f78ea86
chore(category_theory/category/preorder): split material on galois connections (#17339)
kim-em committed 3 years ago
d82b8787
chore(ring_theory/ideal/local_ring): split file (#17319)
urkud committed 3 years ago
c1918ac1
chore(algebra/big_operators): golf 2 proofs (#17345)
urkud committed 3 years ago
315e6cdf
refactor(analysis/complex): use Liouville to prove algebraic closedness (#17343)
alreadydone committed 3 years ago
3642cbed
chore(algebra/group_power/basic): reduce imports (#17334)
kim-em committed 3 years ago
f749197b
chore(data/nat/gcd/basic): remove spurious imports (#17333)
kim-em committed 3 years ago
02812da5
feat(group_theory/abelianization): Add `commutator_representatives` (#17312)
tb65536 committed 3 years ago
0f4c9091
chore(algebra/order/group): split file
kim-em committed 3 years ago
de634da9
feat(analysis/special_functions): the japanese bracket (#16491)
mcdoll committed 3 years ago
c2d9927e
chore(algebra/field/basic): reduce imports (#17331)
kim-em committed 3 years ago
bf3b52da
chore(algebra/regular/basic): split file (#17179)
kim-em committed 3 years ago
acf831c1
feat(algebra/gcd_monoid): extract gcd from multiset/finset (#17316)
alreadydone committed 3 years ago
43cd4142
Revert "chore(data/nat/cast): remove spurious imports"
kim-em committed 3 years ago
ca1b2371
chore(data/nat/cast): remove spurious imports
kim-em committed 3 years ago
d41e9916
feat(measure_theory/measure/measure_space): Add parallel set of lemmas about count (#17245)
kkytola committed 3 years ago
a0381d50
feat(representation_theory/fdRep): Schur's lemma (#13794)
kim-em committed 3 years ago
b9430470
feat(group_theory/index): add 3 lemmas (#17288)
urkud committed 3 years ago
2fc49d57
chore(algebra/order/group/basic): Improve lemma names (#16970)
YaelDillies committed 3 years ago
402f8982
feat(category_theory): nat_trans.equiv_of_comp_fully_faithful (#17304)
joelriou committed 3 years ago
51c07ea9
feat(category_theory/limits/shapes/*): More API around kernel pairs. (#17301)
erdOne committed 3 years ago
f6bab678
feat(representation_theory): fdRep k G is k-linear with finite dimensional hom spaces (#13789)
kim-em committed 3 years ago
ee89acdf
feat(category_theory/limits/shapes/types): Coproducts in `Type` (#17280)
erdOne committed 3 years ago
f020f410
feat(order/topology/filter): define topology on `filter X` (#17219)
urkud committed 3 years ago
78e50d8f
Terms Of Use Privacy Policy Refund Policy Impressum