leanprover-community/mathlib3

Pull Requests Commits

feat(*/pi): add lemmas about how `single` interacts with operators (#6317)

eric-wieser committed 5 years ago

c7c40a7d

chore(*): fix broken Zulip archive links (#6321)

bryangingechen committed 5 years ago

4d2dcdb5

chore(ring_theory/*): split lines (#6316)

Julian-Kuelshammer committed 5 years ago

3e381ad0

refactor(linear_algebra/pi): add `linear_map.single` to match `add_monoid_hom.single` (#6315)

eric-wieser committed 5 years ago

32b9b214

chore(data/indicator_function): add a formula for the support of `indicator` (#6314)

urkud committed 5 years ago

d483bc2c

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

leanprover-community-bot committed 5 years ago

3ab9818f

feat(analysis/calculus): define a smooth bump function (#4458)

urkud committed 5 years ago

845654a1

doc(ring_theory): move some module docstring to correct place (#6312)

jcommelin committed 5 years ago

f6eef43c

doc(ring_theory/witt_vector/witt_polynomial): move module docstring up (#6310)

jcommelin committed 5 years ago

aaab8375

doc(set_theory/*): more documentation about cardinals and ordinals (#6247)

fpvandoorn committed 5 years ago

0df19987

chore(data/buffer/parser/numeral): derive mono for numeral (#5463)

pechersky committed 5 years ago

114f8ef8

fix(lint/type_classes): fix instance_priority bug (#6305)

fpvandoorn committed 5 years ago

e5c77892

chore(topology/Profinite): reduce universe variables (#6300)

kim-em committed 5 years ago

a0e2b3c4

feat(topology/{subset_properties,separation}): closed subsets of compact t0 spaces contain a closed point (#6273)

kmill committed 5 years ago

64d86f7a

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

leanprover-community-bot committed 5 years ago

626a4b57

feat(data/list/basic): tail_drop, cons_nth_le_drop_succ (#6265)

pechersky committed 5 years ago

75149c39

fix(tactic/push_neg): fully simplify expressions not named `h` (#6297)

robertylewis committed 5 years ago

1fecd52f

fix(archive/100/82): remove nonterminal simps (#6299)

fpvandoorn committed 5 years ago

3a8d9769

feat(category_theory/adjunction/reflective): show compositions of reflective are reflective (#6298)

callesonne committed 5 years ago

86969906

perf(tactic/lint/frontend): run linters in parallel (#6293)

gebner committed 5 years ago

96f89335

chore({algebra, algebraic_geometry}/*): move 1 module doc and split lines (#6294)

Julian-Kuelshammer committed 5 years ago

619c1b0d

feat(topology/category/profinite): show Profinite is reflective in CompHaus (#6219)

callesonne committed 5 years ago

5b579a2c

fix(doc/references.bib): fix syntax (#6290)

bryangingechen committed 5 years ago

5a597819

feat(order/pfilter): add preorder filters, dual to preorder ideals (#5928)

mguaypaq committed 5 years ago

2a7eafa5

feat(linear_algebra/dual): adds dual annihilators (#6078)

kex-y committed 5 years ago

017acaee

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

leanprover-community-bot committed 5 years ago

7c267dfa

kim-em committed 5 years ago

1be15889

chore(analysis/normed_space/finite_dimension,topology/metric_space): golf (#6285)

urkud committed 5 years ago

7592a8f4

feat(data/zmod/basic): add simp lemmas about coercions, tidy lemma names (#6280)

eric-wieser committed 5 years ago

bc1c4f24

feat(analysis/normed_space/multilinear): generalized `curry` (#6270)

urkud committed 5 years ago

75f33464

Newer Older