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

chore(algebra/order/group): split file

kim-em committed 3 years ago

de634da9

kim-em committed 3 years ago

a361e1e7

kim-em committed 3 years ago

6d6553b5

kim-em committed 3 years ago

1f5c7d03

kim-em committed 3 years ago

3b58be2c

add missing downstream imports

kim-em committed 3 years ago

da238e07

Merge branch 'pointwise_interval' into sup

kim-em committed 3 years ago

d5cb2b00

kim-em committed 3 years ago

f030bdf4

kim-em committed 3 years ago

19e44ea1

kim-em committed 3 years ago

ae26d7b6

Merge branch 'pnat' into sup

kim-em committed 3 years ago

39a254a2

kim-em committed 3 years ago

976fcb01

kim-em committed 3 years ago

3cb5d94a

suggestion from review

kim-em committed 3 years ago

3e2b1264

kim-em committed 3 years ago

5bb11af8

kim-em committed 3 years ago

14a8ad7e

chore(algebra/order/field): split out file about powers

kim-em committed 3 years ago

384a9b00

kim-em committed 3 years ago

99ac1d3b

kim-em committed 3 years ago

327b61ad

kim-em committed 3 years ago

49da2760

kim-em committed 3 years ago

1882bfe7

kim-em committed 3 years ago

ceb95a0a

Merge branch 'pointwise_interval' into sup

kim-em committed 3 years ago

dcbd5c86

Newer Older