leanprover-community/mathlib

Pull Requests Commits

foxthomson committed 4 years ago

d6ebc42e

Merge branch 'master' into is_regular

foxthomson committed 4 years ago

bc05a352

chore(measure_theory/measure_space): add some `simp`/`mono` tags (#6221)

urkud committed 4 years ago

ad5a81d3

feat(measure_theory/measure_space): add ae_imp_iff (#6218)

RemyDegenne committed 4 years ago

3cfaa0bf

feat(measure_theory/borel_space): add ae_measurable versions of finset.measurable_prod and measurable.ennreal_tsum (#6217)

RemyDegenne committed 4 years ago

d0456d3b

feat(ring_theory/ideal/operations): add first isomorphism theorem for rings and algebras (#6166)

riccardobrasca committed 4 years ago

42bb0c4b

feat(linear_algebra/pi_tensor_product): tmul distributes over tprod (#6126)

eric-wieser committed 4 years ago

8b59d97d

refactor(topology/{basic,continuous_on}): review `continuous_if` etc (#6182)

urkud committed 4 years ago

445e6fc0

doc(data/polynomial/denoms_clearable): fix typo in the doc-string (#6174)

adomani committed 4 years ago

5c22531b

feat(data/int/gcd): some missing lemmas about int.gcd (#6212)

digama0 committed 4 years ago

5bee8262

chore(analysis/special_functions/pow): review lemmas about measurability of `cpow`/`rpow` (#6209)

urkud committed 4 years ago

0544641d

chore(topology/algebra/module): review `coe` lemmas (#6206)

urkud committed 4 years ago

ee9197a1

chore(group_theory/free_group): clean up unnecessary lemmas (#6200)

eric-wieser committed 4 years ago

43bfd903

chore(analysis/calculus/local_extr): minor golfing (#6214)

urkud committed 4 years ago

759ebc0b

chore(scripts): update nolints.txt (#6213)

leanprover-community-bot committed 4 years ago

5869039e

doc(docs/overview.yaml): Added Hall's theorem (#6205)

kmill committed 4 years ago

37459eee

chore(algebra/group/pi): replace a lemma with @[simps] (#6203)

eric-wieser committed 4 years ago

06fdc087

feat(number_theory/ADE_inequality): the inequality 1/p + 1/q + 1/r > 1 (#6156)

jcommelin committed 4 years ago

e79bf053

feat(data/fin): cast_succ_mk and other lemmas (#6094)

kim-em committed 4 years ago

30c2c5bf

feat(measure_theory/measure_space): add theorems about restrict and subtraction (#5000)

mzinkevi committed 4 years ago

152ad1fc

feat(data/set/intervals/basic): 24 lemmas about membership of arithmetic operations (#6202)

eric-wieser committed 4 years ago

dd13f00a

foxthomson committed 4 years ago

Verified 06cd5999

Docstring formatting

foxthomson committed 4 years ago

Verified a4b4da15

foxthomson committed 4 years ago

Verified 83f9c526

foxthomson committed 4 years ago

Verified 9d41195c

feat(analysis/special_functions/exp_log): added `log_div` (#6196)

benjamindavidson committed 4 years ago

254c3ee1

feat(analysis/calculus): generalize `has_strict_fderiv_at.map_nhds_eq` (#6193)

urkud committed 4 years ago

a5ccba6b

fix(topology/topological_fiber_bundle): fix definition, review (#6184)

urkud committed 4 years ago

74d3270e

feat(topology/subset_properties): compact discrete spaces are finite (#6191)

jcommelin committed 4 years ago

2d708803

chore(scripts): update nolints.txt (#6194)

leanprover-community-bot committed 4 years ago

159e807b

Older