leanprover-community/mathlib

Pull Requests Commits

YaelDillies committed 4 years ago

bed5cda1

feat(algebra/ordered_ring): `a + 1 ≤ 2 * a` (#7995)

adomani committed 4 years ago

767901ab

chore(analysis/special_functions): move measurability statements to measure_theory folder (#8006)

sgouezel committed 4 years ago

fae00c7c

chore(analysis/liouville/liouville + data/real/liouville): create folder `analysis/liouville/`, move `data/real/liouville` into new folder (#7998)

adomani committed 4 years ago

547df12b

feat(measure_theory/interval_integral): integral of a non-integrable function (#8011)

benjamindavidson committed 4 years ago

3a0f2822

refactor(topology/metric_space/isometry): move material about isometries of normed spaces (#8003)

hrmacbeth committed 4 years ago

7d155d95

feat(algebra/homology/homotopy): flesh out the api a bit, add some simps (#7941)

jcommelin committed 4 years ago

7d5b50a7

chore(data/int/basic): rationalize the arguments implicitness (mostly to_nat_sub_of_le) (#7997)

YaelDillies committed 4 years ago

63c3ab56

chore(topology/metric_space/pi_Lp): move to analysis folder, import inner_product_space (#7991)

sgouezel committed 4 years ago

cd8f7b5c

chore(analysis/mean_inequalities): split integral mean inequalities to a new file (#7990)

sgouezel committed 4 years ago

497b84d2

feat(measure_theory/interval_integral): `abs_integral_le_integral_abs` (#7959)

benjamindavidson committed 4 years ago

1846a1f3

feat(data/{fin,nat,zmod}): prove `zmod.coe_add_eq_ite` (#7975)

Vierkantor committed 4 years ago

2ca04524

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

leanprover-community-bot committed 4 years ago

28aee951

feat(category_theory/yoneda): develop API for representable functors (#7962)

b-mehta committed 4 years ago

2a48c690

feat(group_theory): computable 1st isomorphism theorem (#7988)

Vierkantor committed 4 years ago

42ab44c2

feat(measure_theory): links between an integral and its improper version (#7164)

ADedecker committed 4 years ago

3ee6248c

docs(data/set/enumerate): add module and definition docstrings (#7967)

YaelDillies committed 4 years ago

f2f10cce

feat(data/real/ennreal): add a `algebra ℝ≥0 ℝ≥0∞` instance (#7846)

eric-wieser committed 4 years ago

3a0653c7

chore(topology/basic): rename compact_Icc to is_compact_Icc (#7979)

sgouezel committed 4 years ago

52dbff0f

feat(topology/algebra/ordered, topology/algebra/infinite_sum): bounded monotone sequences converge (variant versions) (#7983)

hrmacbeth committed 4 years ago

29e7a8d5

feat(analysis/convex/basic): missing lemmas (#7946)

YaelDillies committed 4 years ago

7c9a8113

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

leanprover-community-bot committed 4 years ago

e168bf7a

chore(order/iterate): fix up the namespace (#7977)

YaelDillies committed 4 years ago

49bf1fde

docs(data/*/sqrt): add one module docstring and expand the other (#7973)

YaelDillies committed 4 years ago

dc73d1bd

docs(data/list/intervals): add module docstring (#7972)

YaelDillies committed 4 years ago

3824a43e

docs(data/int/range): add module docstring (#7971)

YaelDillies committed 4 years ago

93d7812a

docs(data/int/cast): add module docstring (#7969)

YaelDillies committed 4 years ago

da1a32c2

docs(data/nat/dist): add module docstring (#7966)

YaelDillies committed 4 years ago

de6d739d

feat(topology/locally_constant): Adds a few useful constructions (#7954)

adamtopaz committed 4 years ago

ce23f373

docs(data/nat/cast): add module docstring (#7947)

YaelDillies committed 4 years ago

e9f9f3f3

Older