leanprover-community/mathlib

Pull Requests Commits

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

chore(data/list/prod): remove an out of date comment (#11058)

alexjbest committed 3 years ago

34e79d6c

chore(ring_theory/polynomial/bernstein): use `∑` notation (#11060)

urkud committed 3 years ago

266d12be

feat(algebraic_geometry): Results about open immersions of schemes. (#10977)

erdOne committed 3 years ago

abf96572

feat(data/int/basic): add lemma `gcd_greatest` (#10613)

stuart-presnell committed 3 years ago

07b578e5

split(algebra/big_operators/multiset): Split off `data.multiset.basic` (#11043)

YaelDillies committed 3 years ago

8d426f04

chore(set_theory/ordinal): Removed redundant argument from `enum_typein` (#11049)

vihdzp committed 3 years ago

4923cfc5

feat(data/set/basic): Added `range_eq_iff` (#11044)

vihdzp committed 3 years ago

ad99529e

chore(data/real/ennreal): adjust form of `to_real_pos_iff` (#11047)

hrmacbeth committed 3 years ago

914250ef

chore(data/matrix/block): Eliminate `finish` (#10948)

stuart-presnell committed 3 years ago

c9f47c97

feat(measure_theory/integral): define `circle_integral` (#10906)

urkud committed 3 years ago

0aca7061

chore(category_theory/limits) : Remove instance requirement (#11041)

erdOne committed 3 years ago

ef8005cd

chore(measure_theory/function/lp_space): use notation for `nnnorm` (#11039)

hrmacbeth committed 3 years ago

864a12e8

chore(algebra/*): Eliminate `finish` (#11034)

stuart-presnell committed 3 years ago

0f076d24

feat(ring_theory/localization): The localization at a fg submonoid is of finite type. (#10990)

erdOne committed 3 years ago

f9561d40

feat(data/nat/totient): add totient_mul_prime_div (#10971)

riccardobrasca committed 3 years ago

5719a029

feat(combinatorics/configuration): Points and lines inequality (#10772)

tb65536 committed 3 years ago

d28b3bd5

Newer Older