leanprover-community/mathlib

Pull Requests Commits

kim-em committed 4 years ago

54d0d9b3

Merge branch 'connective' into hexp

kim-em committed 4 years ago

8f510540

kim-em committed 4 years ago

0b27685c

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

leanprover-community-bot committed 4 years ago

626a4b57

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

pechersky committed 4 years ago

75149c39

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

robertylewis committed 4 years ago

1fecd52f

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

fpvandoorn committed 4 years ago

3a8d9769

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

callesonne committed 4 years ago

86969906

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

gebner committed 4 years ago

96f89335

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

Julian-Kuelshammer committed 4 years ago

619c1b0d

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

callesonne committed 4 years ago

5b579a2c

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

bryangingechen committed 4 years ago

5a597819

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

mguaypaq committed 4 years ago

2a7eafa5

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

kex-y committed 4 years ago

017acaee

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

leanprover-community-bot committed 4 years ago

7c267dfa

kim-em committed 4 years ago

1be15889

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

urkud committed 4 years ago

7592a8f4

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

eric-wieser committed 4 years ago

bc1c4f24

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

urkud committed 4 years ago

75f33464

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

kim-em committed 4 years ago

152bf15a

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

eric-wieser committed 4 years ago

4bae1c47

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

awainverse committed 4 years ago

07a1b8db

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

ocfnash committed 4 years ago

f066eb1a

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

urkud committed 4 years ago

d43a3bae

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

kim-em committed 4 years ago

b190131f

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

kim-em committed 4 years ago

8b8a5a27

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

urkud committed 4 years ago

ea1cff4a

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

AdrianDoM committed 4 years ago

0c61fc46

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

benjamindavidson committed 4 years ago

9b3008eb

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

faenuccio committed 4 years ago

3c157512

Older