leanprover-community/mathlib

Pull Requests Commits

AlexKontorovich committed 3 years ago

78b555a0

hyperbola sketch proof

b-mehta committed 3 years ago

9450a0c3

Merge branch 'ant-estimates' of https://github.com/leanprover-community/mathlib into ant-estimates

AlexKontorovich committed 3 years ago

7f14fcc0

AlexKontorovich committed 3 years ago

a571b366

b-mehta committed 3 years ago

Verified 4337f5c2

move around statements

b-mehta committed 3 years ago

1a2195c5

chebyshev inequalities

b-mehta committed 3 years ago

a76ac816

a bunch of estimates!

b-mehta committed 3 years ago

c9f96d71

Merge branch 'master' into ant-estimates

b-mehta committed 3 years ago

03cc46f7

Improved partial summation proof

b-mehta committed 3 years ago

Verified 545ae2f7

Merge branch 'master' into ant-estimates

b-mehta committed 3 years ago

Verified 32f47828

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

YaelDillies committed 3 years ago

294e78e7

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

digama0 committed 3 years ago

1332fe1a

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

tb65536 committed 3 years ago

0e8cca36

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

tb65536 committed 3 years ago

6ed17fc7

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

stuart-presnell committed 3 years ago

e1133ccc

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

YaelDillies committed 3 years ago

46566c5b

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

urkud committed 3 years ago

2ecf4800

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

stuart-presnell committed 3 years ago

de6f57d2

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

kmill committed 3 years ago

d67c4697

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

YaelDillies committed 3 years ago

ca2c3443

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

eric-wieser committed 3 years ago

463be884

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

erdOne committed 3 years ago

a3603547

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

kmill committed 3 years ago

ae8f08fe

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

stuart-presnell committed 3 years ago

f525f93e

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

riccardobrasca committed 3 years ago

2f3b966f

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

pechersky committed 3 years ago

002b8d97

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

huynhtrankhanh committed 3 years ago

b28734c8

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

ocfnash committed 3 years ago

7e0b994c

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

tb65536 committed 3 years ago

7c9ce5c0

Older