leanprover-community/mathlib

Pull Requests Commits

use general proof

robertylewis committed 4 years ago

8c1b6c0e

generalize linear_map.bound_of_ball_bound'

robertylewis committed 4 years ago

49c4e8cb

robertylewis committed 4 years ago

05578577

robertylewis committed 4 years ago

6b1d05f0

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

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

urkud committed 4 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

Older