Commits leanprover-community/mathlib3

feat(analysis/specific_limits): formula for `∑' n, n * r ^ n` (#5835)

urkud committed 4 years ago

507c7ffc

chore(linear_algebra/multilinear): Relax ring to semiring, add_comm_group to add_comm_monoid (#5870)

eric-wieser committed 4 years ago

5222db01

Add collapsed quantifiers to clipboard paste code.

EdAyers committed 4 years ago

91c5f4d8

feat(order/complete_well_founded, data/finset/lattice): introduce compact elements of a complete lattice and characterize compact lattices as those with all elements compact (#5825)

cemulate committed 4 years ago

fbabe427

Add note regarding addressing bug

EdAyers committed 4 years ago

564e91f5

Remove list.subtract

EdAyers committed 4 years ago

a5ded233

Merge branch 'master' into collapse-restricted-quantifiers

EdAyers committed 4 years ago

9bc2b801

feat(data/nat/basic): add decidable_exists_lt deciding existence of a natural below a bound satisfying a predicate (#5864)

alexjbest committed 4 years ago

5db7a188

feat(measure_theory/lp_space): define Lp, subtype of ae_eq_fun with finite norm (#5853)

RemyDegenne committed 4 years ago

49c53d4f

feat(topology/subset_properties): a locally compact space with second countable topology is sigma compact (#5689)

fpvandoorn committed 4 years ago

aa744dba

feat(analysis/analytic/composition): filling small holes in existing API (#5822)

sgouezel committed 4 years ago

f414fcaa

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

leanprover-community-bot committed 4 years ago

160d243d

feat(algebra/pointwise): a lemma about pointwise addition/multiplication of bdd_above sets (#5859)

alexjbest committed 4 years ago

8da574f5

refactor(analysis/analytic/composition): extend definition, extract a lemma from a proof (#5850)

sgouezel committed 4 years ago

3a136f81

chore(set_theory/ordinal): use rel_iso notation in ordinal (#5857)

alexjbest committed 4 years ago

74760f22

feat(order/rel_iso): generalise several lemmas to assume only has_le not preorder (#5858)

alexjbest committed 4 years ago

013b902d

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

leanprover-community-bot committed 4 years ago

b0e874e0

docs(undergrad.yaml): update with #5724 and #5788 (#5855)

hrmacbeth committed 4 years ago

04972f69

feat(analysis/mean_inequalities, measure_theory/lp_space): extend mem_Lp.add to all p in ennreal (#5828)

RemyDegenne committed 4 years ago

3250fc30

feat(algebra/lie/basic): define the radical of a Lie algebra and prove it is solvable (#5833)

ocfnash committed 4 years ago

f48ce7ec

feat(analysis/analytic): a continuous linear map defines an analytic function (#5840)

urkud committed 4 years ago

cb618e01

chore(algebra/group_power): generalize `semiring` version of Bernoulli's inequality (#5831)

urkud committed 4 years ago

faba9cea

feat(measure_theory/interval_integral) : add integration by parts (#5724)

mmasdeu committed 4 years ago

0feb1d20

feat(order/modular_lattice): define modular lattices (#5564)

awainverse committed 4 years ago

de10203f

chore(data/nat/basic): reuse a proof, drop a duplicate (#5836)

urkud committed 4 years ago

38ae9b37

feat(data/polynomial/algebra_map): aeval_map (#5843)

tb65536 committed 4 years ago

8b4c455b

feat(field_theory/minpoly): Minimal polynomials of degree one (#5844)

tb65536 committed 4 years ago

bef50a4d

feat(topology/metric_space/{basic,emetric_space}): product of balls of the same size (#5846)

urkud committed 4 years ago

6958d8cd

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

leanprover-community-bot committed 4 years ago

244b3ed0

chore(analysis/analytic/composition): minor golfing (#5839)

urkud committed 4 years ago

c681f48c