leanprover-community/mathlib

Pull Requests Commits

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

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

feat(data/fin): pred_above_monotone (#6170)

kim-em committed 5 years ago

152bf15a

doc(tactic/algebra): document @[ancestor] (#6272)

eric-wieser committed 5 years ago

4bae1c47

feat(ring_theory/simple_module): introduce `is_semisimple_module` (#6215)

awainverse committed 5 years ago

07a1b8db

feat(algebra/lie/subalgebra): define lattice structure for Lie subalgebras (#6279)

ocfnash committed 5 years ago

f066eb1a

feat(analysis/normed_space/inner_product): norm is smooth at `x ≠ 0` (#6275)

urkud committed 5 years ago

d43a3bae

feat(data/int/basic): lemmas about int and int.to_nat (#6253)

kim-em committed 5 years ago

b190131f

feat(category/eq_to_hom): lemmas to replace rewriting in objects with eq_to_hom (#6252)

kim-em committed 5 years ago

8b8a5a27

feat(linear_algebra/pi): ext lemma for `f : (Π i, M i) →ₗ[R] N` (#6233)

urkud committed 5 years ago

ea1cff4a

feat(group_theory): prove the 2nd isomorphism theorem for groups (#6187)

AdrianDoM committed 5 years ago

0c61fc46

feat(algebra/ordered_monoid): inequalities involving mul/add (#6171)

benjamindavidson committed 5 years ago

9b3008eb

feat(ring_theory/ideal/operations) : add lemma prod_eq_bot (#5795)

faenuccio committed 5 years ago

3c157512

Newer Older