leanprover-community/mathlib3

Pull Requests Commits

feat(measure_theory/integral/{interval,circle}_integral): add strict inequalities (#11061)

urkud committed 3 years ago

c04a42fe

feat(data/pi): bit[01]_apply simp lemmas (#11086)

pechersky committed 3 years ago

f452b383

feat(tactic/fin_cases): document `fin_cases with` and add `fin_cases using` (#11085)

robertylewis committed 3 years ago

94bb4667

feat(ring_theory/power_series/basic): add api for coeffs of shifts (#11082)

alexjbest committed 3 years ago

44f22aac

feat(data/set/finite): finite_or_infinite (#11084)

kmill committed 3 years ago

f0ca4338

feat(ring_theory/polynomial/cyclotomic/basic): add cyclotomic_expand_eq_cyclotomic (#10974)

riccardobrasca committed 3 years ago

612a4766

feat(ring_theory/polynomial/cyclotomic/basic): cyclotomic_prime_mul_X_sub_one (#11063)

ericrbg committed 3 years ago

10ea8609

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

chore(analysis/complex/circle): minor review (#11059)

urkud committed 3 years ago

4f02336c

feat(data/pi/interval): Dependent functions to locally finite orders are locally finite (#11050)

YaelDillies committed 3 years ago

daab3ac4

chore(logic/small): Some golfing (#11030)

vihdzp committed 3 years ago

2e2510ee

feat(measure_theory/integral): a couple of lemmas on integrals and integrability (#10983)

b-mehta committed 3 years ago

dd6707c9

Older