leanprover-community/mathlib

Pull Requests Commits

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

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

feat(finite_dimensional/subalgebra) : add subalgebra.is_simple_order_of_finrank (#17237)

xroblot committed 3 years ago

6d8e6ead

feat(linear_algebra/affine_space/basis): add `affine_basis.finite_dimensional` (#17246)

urkud committed 3 years ago

aae5e52b

feat(category_theory/triangulated): changing namespaces, introducing triangulated categories (#17284)

joelriou committed 3 years ago

19786714

feat(order/upper_lower): Upper sets correspond to monotone predicates (#17241)

YaelDillies committed 3 years ago

c64b2b4b

chore(data/nat/basic): reorder arguments to `nat.even_odd_rec` to make it work with `induction` (#17165)

eric-wieser committed 3 years ago

57035e18

chore(*): fix some to_additive orders (#17297)

alexjbest committed 3 years ago

b566cd5a

feat(analysis/normed/group/basic): closure of `{0}` in a seminormed group (#17287)

ADedecker committed 3 years ago

fdc3136d

feat(linear_algebra): lemmas and instances on cardinality of quotients (#17084)

Vierkantor committed 3 years ago

7e2084a7

Newer Older