leanprover-community/mathlib3

Pull Requests Commits

b-mehta committed 4 years ago

f51c208a

b-mehta committed 4 years ago

f6d6f9d0

b-mehta committed 4 years ago

b234a25f

b-mehta committed 4 years ago

a424e6dc

b-mehta committed 4 years ago

b90c1b10

Merge branch 'ant-estimates' into ant-estimates-bm

b-mehta committed 4 years ago

4a3c381b

Merge branch 'master' into ant-estimates

b-mehta committed 4 years ago

03cc46f7

b-mehta committed 4 years ago

553cef0c

Improved partial summation proof

b-mehta committed 4 years ago

Verified 545ae2f7

Merge branch 'master' into ant-estimates

b-mehta committed 4 years ago

Verified 32f47828

feat(algebra/group_with_zero/power): With zero lemmas (#11051)

YaelDillies committed 4 years ago

294e78e7

fix(tactic/rcases): more with_desc fail (#11004)

digama0 committed 4 years ago

1332fe1a

feat(algebra/big_operators/order): `prod_eq_prod_iff_of_le` (#11068)

tb65536 committed 4 years ago

0e8cca36

refactor(combinatorics/configuration): Generalize results (#11065)

tb65536 committed 4 years ago

6ed17fc7

chore(order/*): Eliminate `finish` (#11064)

stuart-presnell committed 4 years ago

e1133ccc

split(data/list/infix): Split off `data.list.basic` (#11062)

YaelDillies committed 4 years ago

46566c5b

feat(algebra/group/units): generalize `units.coe_lift` (#11057)

urkud committed 4 years ago

2ecf4800

chore(ring_theory/unique_factorization_domain): Eliminate `finish` (#11055)

stuart-presnell committed 4 years ago

de6f57d2

feat(combinatorics/simple_graph/basic): edge deletion (#11054)

kmill committed 4 years ago

d67c4697

split(data/finsupp/order): Split off `data.finsupp.basic` (#11045)

YaelDillies committed 4 years ago

ca2c3443

feat(algebra/group_with_zero): add zero_mul_eq_const and mul_zero_eq_const (#11021)

eric-wieser committed 4 years ago

463be884

feat(algebraic_geometry): Basic open set is empty iff section is zero in reduced schemes. (#11012)

erdOne committed 4 years ago

a3603547

feat(combinatorics/simple_graph/connectivity): more lemmas (#11010)

kmill committed 4 years ago

ae8f08fe

chore(*): Eliminate `finish` (#10970)

stuart-presnell committed 4 years ago

f525f93e

feat(number_theory/cyclotomic/basic): add is_cyclotomic_extension (#10849)

riccardobrasca committed 4 years ago

2f3b966f

feat(algebra/group_with_zero/basic): mul_{left,right}_eq_self₀ (#11069)

pechersky committed 4 years ago

002b8d97

feat(data/sym): Provide API for data.sym (#11032)

huynhtrankhanh committed 4 years ago

b28734c8

feat(topology/compact_convergence): define compact convergence (#10967)

ocfnash committed 4 years ago

7e0b994c

feat(algebra/order/monoid_lemmas): `mul_eq_mul_iff_eq_and_eq` (#11056)

tb65536 committed 4 years ago

7c9ce5c0

further attempts

b-mehta committed 4 years ago

d42782da

Older