leanprover-community/mathlib3

Pull Requests Commits

awainverse committed 3 years ago

3947d6ea

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 4 years ago

daab3ac4

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

vihdzp committed 4 years ago

2e2510ee

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

b-mehta committed 4 years ago

dd6707c9

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

alexjbest committed 4 years ago

34e79d6c

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

urkud committed 4 years ago

266d12be

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

erdOne committed 4 years ago

abf96572

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

stuart-presnell committed 4 years ago

07b578e5

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

YaelDillies committed 4 years ago

8d426f04

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

vihdzp committed 4 years ago

4923cfc5

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

vihdzp committed 4 years ago

ad99529e

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

hrmacbeth committed 4 years ago

914250ef

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

stuart-presnell committed 4 years ago

c9f47c97

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

urkud committed 4 years ago

0aca7061

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

erdOne committed 4 years ago

ef8005cd

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

hrmacbeth committed 4 years ago

864a12e8

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

stuart-presnell committed 4 years ago

0f076d24

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

erdOne committed 4 years ago

f9561d40

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

riccardobrasca committed 4 years ago

5719a029

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

tb65536 committed 4 years ago

d28b3bd5

feat(algebraic_geometry): Schemes are sober. (#11040)

erdOne committed 4 years ago

0dd60aeb

feat(measure_theory/measure/haar_lebesgue): Lebesgue measure of the image of a set under a linear map (#11038)

sgouezel committed 4 years ago

f80c18bf

chore(algebraic_geometry): Remove unwanted spaces. (#11042)

erdOne committed 4 years ago

aa669096

feat(data/mv_polynomial): API for mv polynomial.rename (#10921)

isadofschi committed 4 years ago

d6ecc14a

feat(analysis/inner_product_space/adjoint): show that continuous linear maps on a Hilbert space form a C*-algebra (#10837)

dupuisf committed 4 years ago

f7038c24

feat(combinatorics/configuration): Inequality between `point_count` and `line_count` (#11036)

tb65536 committed 4 years ago

8a997f3f

feat(measure_theory/covering/besicovitch): covering a set by balls with controlled measure (#11035)

sgouezel committed 4 years ago

8181fe89

refactor(data/nat/prime): redefine nat.prime as irreducible (#11031)

Ruben-VandeVelde committed 4 years ago

a998db66

feat(data/multiset/basic): empty_or_exists_mem (#11023)

ericrbg committed 4 years ago

3588c3a0

Older